International justice and privacy

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:

Preliminary results are presented in:

Quick instructions to install and test

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.