UKano: UnlinKability and ANOnymity verifier v0.6
UKano is a modified version of the ProVerif tool including automatic verification of anonymity and unlinkability of 2-agents protocols. See the UKano webpage for more details about the tools and references HBD19 & HBD16 given below for more details on the underlying theory.
You need OCaml >=3.00 (you can find Objective Caml at http://ocaml.org).
The executable program
proverif have been built.
You can also build UKano only by typing
UKano needs an exectuable of ProVerif though. Refer to the manual
for the required version.
To quickly test the tool on our case studies: build it, choose an example
in the examples folder (e.g.,
To test the tool against examples with known expected conclusions, you can also type
To run UKano on a protocol written in
filename (compliant with ProVerif typed format), use
The tool describes the main steps it follows and concludes whether unlinkability
and anonymity could be established or not. Type
./ukano --help to see the list
of options of UKano.
How Does It Work?
We have proved in HBD19 (preliminary versions in HBD16,H17) that, for 2-party protocols, unlinkability and anonmyity follow from two sufficent conditions we called Frame Opacity (FO) and Well-Authentication (WA). We also show how to verify those two conditions relying on dedicated encodings. UKAno mechanizes all those encodings.
After parsing your file, the tool creates two other files in the same
directory. Each file encodes one of our two sufficient conditions.
The one encoding FO is suffixed with
_FOpa.pi. The second suffixed
_WAuth.pi can be used to check WA. The latter contains one query
UKano then launches
proverif on those two files and parses the results
in order to conclude whether both conditions have been established. In such
a case, the tool concludes that the input protocol ensures unlinkability and
A complete manual for the tool can be found at https://github.com/LCBH/UKano/wiki. It notably describes the expected format for input files of UKano. You can find a comprehensive list of case studies and benchmarks described in the corresponding section of the manual: https://github.com/LCBH/UKano/wiki#our-case-studies.
[H17]: L. Hirschi. PhD Thesis. Automated Verification of Privacy in Security Protocols: Back and Forth Between Theory & Practice. A copy is available at http://www.lsv.fr/~hirschi/defense.php.
[HBD16]: 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. A copy can be found at http://projects.lsv.ens-cachan.fr/ukano/.