UKano: automatic privacy verifier

UKano

UKano: Automatic Privacy Verifier

This tool automatically checks unlinkability and anonymity for a large class of 2-party protocols for an unbounded number of sessions.

It has been successfully applied on various real-life authentication protocols (e.g., ePassport and RFID protocols) to establish privacy properties and find privacy threats.

The tool UKano and expermiental results are formally described in:

L. Hirschi, D. Baelde and S. Delaune. A method for unbounded verification of privacy-type properties. In Under submission to the Journal of Computer Security (JCS), IOS Press. Journal paper (PDF).

Preliminary results are presented in:

L. Hirschi, D. Baelde and S. Delaune. A Method for Verifying Privacy-Type Properties : The Unbounded Case. In IEEE Symposium on Security and Privacy (Oakland), 2016. Paper (PDF).

L. Hirschi, Automated Verification of Privacy in Security Protocols: Back and Forth Between Theory & Practice. PhD Thesis. Manuscript (PDF).

UKano releases, manual and repository
Journal paper (most up-to-date) and Oakland'16 paper
List of our cases studies and benchmarks

Quick instructions to install and test

Download the last release of UKano here (currently v0.3) and unpack.
You need OCaml >=3.00 (you can find Objective Caml at ocaml.org).
Just type: make.
The executable program ukano and proverif have been built.
To quickly test the tool on our case studies: build it, choose a case study in ./examples/ (e.g., ./examples/Feldhofer/feldhofer.pi and launch ukano. For instance: ./ukano examples/Feldhofer/feldhofer.pi.
See the README or the manual for more details.

UKano is built on top of ProVerif v1.97, an automatic cryptographic protocol verifier in the symbolic model.

UKano is developed by Lucca Hirschi. Last update: October 5th 2017.