Skip to content

Home

Jump to bottom
LCBH edited this page Feb 8, 2017 · 24 revisions

UKano: UnlinKability and ANOnymity verifier

Lucca Hirschi
http://projects.lsv.ens-cachan.fr/ukano/

UKano is a modified version of the ProVerif tool including automatic verification of anonymity and unlinkability of 2-agents protocols. See references HBD16 & H17 given below for more details on the underlying theory.

Install

You need OCaml >=3.00 (you can find Objective Caml at http://ocaml.org). Just type: make. The executable program ukano and proverif have been built.

You can also build UKano only by typing make ukano. UKano needs an exectuable of ProVerif though. You can specify the path of your ProVerif executable with the option --proverif <path>.

Quick Test

To quickly test the tool on our case studies: build it, choose an example in the examples folder (e.g., ./examples/Feldhofer/feldhofer.pi) and type ./ukano <path-example>.

To test the tool against examples with known expected conclusions, you can also type make test.

Usage

Basic

To run UKano on a protocol written in filename (compliant with ProVerif typed format, see Section Expected Format for more details of this format), use

./ukano <filename>

The tool describes the main steps it follows and concludes whether unlinkability and anonymity could be established or not.

How it works?

We have proved in HBD16 and 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 with _WAuth.pi can be used to check WA. The latter contains a query per conditional. UKano then launches proverif on those two files and parse 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 anonymity.

The folder ./examples/ contains some ProVerif files in the expected format (e.g., ./examples/Feldhofer/feldhofer.pi). They can be used as a starting point to write your own protocols.

Options

Here are the options you may use:

$ ./ukano --help
UKano v0.2 : Cryptographic privacy verifier, by Lucca Hirschi. Based on Proverif v1.91, by Bruno Blanchet and Vincent Cheval.
  --proverif            path of the ProVerif executable to use (optional, default: './proverif')
  --ideal-no-check      assume the idealisation is conform (requires manual checks)
  --ideal-automatic     do not take given diealisations into account, generate them automatically instead
  --ideal-greedy        modifies the idealisation heuristic: put fresh names for all non-tuple sub-terms
  --ideal-full-syntax   modifies the idealisation heuristic: go through all functions (including ones in equations) and replace identity names and let variables by holes. Conformity checks are modified accordingly.
  --only-fo             verifies the frame opacity condition only
  --only-wa             verifies the well-authentication condition only
  --clean               remove generated files after successful verification
  --less-verbose        reduce the verbosity
  --log-proverif        log in stdout all ProVerif outputs
  -gc                   display gc statistics

Some options are described in the next section.

Idealisations Heuristics

We now describe the heuristic UKano uses by default to guess idealisations automatically. Given a syntactic output u in some role, we recursively build an idealisation by case analysis on u:

  1. a constant, we let u be its idealisation
  2. a session name, we let u be its idealisation
  3. a name that is not a session name, we let a new session name be its idealisation (but two occurrences of the same name will be idealised with the same session name)
  4. a variable bind by an input, we let u be its idealisation
  5. variable bind by a let, we let a fresh session name be its idealisation (but two occurrences of the same variable will be idealised with the same session name)
  6. u=f(u1,...,un), vi are idealisations of ui and f does not occur in equations then we let f(v1,...,vn) be the idealisation of u
  7. u=f(u1,...,un) and f does occur in equations then we let a fresh session name be the idealisation of u

The options --ideal-greedy and --ideal-full-syntax allows to modify the above heuristic:

  • --ideal-greedy replaces the cases 6. and 7. as follows: when f is not a tuple then the idealisation is a fresh session name, otherwise we proceed as in 6.
  • --ideal-full-syntax removes the case 7 and removes the condition "f does not occur in equations " in case 6. In case the protocol is in the shared case, UKano then displays a warning message saying that the user should verify WA item (ii) separately.

UKano checks the conformity of guessed idealisations as well as idealisations given by the user. Those checks can be bypassed using the option --ideal-no-check.

The option --ideal-automatic makes UKano bypass idealisations given in input files and automatically guess idealisations instead.

Expected Format

Only typed ProVerif files are accepted (proverif should successfully parse it when using the option -in pitype). Please refer to the manual of ProVerif at the Proverif webpage. Additionally, the file should not define new types and only use types bitstring and channel. The file must declare at least one channel c (i.e., contains a line free c:channel.).

After the definition of the equational theory (without any declaration of events), the inputted file should contain a commentary:

       (* ==PROTOCOL== *)

and then define only one process corresponding to the whole multiple sessions system. This process should satisfy the syntactical restrictions described in H17. However, multiple tests (conditional or evaluation) can be performed in a row between an input and an output if the corresponding else branches are the same. You can also use most of syntactical sugars allowed by ProVerif (e.g., modular definitions through definitions of functions and call, etc.). Finally, to check anonymity as well, identity names to be revealed (and only them) must have id as prefix (e.g., idName).

Improve Precision

Note that, currently, UKano does not detect safe conditionals and consider all conditionals unsafe by default. UKano lists conditionals for which WA could not be established. You should check that they correspond to safe conditionals.

If the tool cannot guess idealisations of outputs (to check frame opacity), you can play with the options described in Section Idealisations Heuristics or compute them manually and add it to the file as explained next.

Output messages that cannot be guessed automatically should be of the form: choice[u,uh] where u is the real message outputted by the protocol and uh is the idealised message. If you define in the equational theory a constant hole (by adding this line: free hole:bitstring.) then all hole will be replaced by fresh and pairwise distinct session names.

Finally, when frame opacity cannot be checked directly, it is sometimes possible to make ProVerif prove it just by slightly modifying the file without altering the underlying protocol (for instance, by moving creation of names).

Our Case Studies

We have tested UKano on several real-world case studies. We list them all below. They all have a dedicated folder in ./examples/.

Legend:

  • ✅ : means that the corresponding condition or property could be automatically established using UKano
  • ❌ : when a condition fails to hold or could not be established
  • 🔥 : when an attack has been found
Protocol Frame-Opacity Well-Authentication Unlinkability
Hash-Lock ✅ ✅ ✅
LAK (stateless) -- ❌ 🔥
Fixed LAK ✅ ✅ ✅
BAC ✅ ✅ ✅
BAC+ PA + AA ✅ ✅ ✅
BAC+ AA + PA ✅ ✅ ✅
PACE (faillible dec) -- ❌ 🔥
PACE (as in~BFK-09) -- ❌ 🔥
PACE -- ❌ 🔥
PACE with tags ✅ ✅ ✅
DAA sign ✅ ✅ ✅
DAA join ✅ ✅ ✅
abcdh (irma) ✅ ✅ ✅

You can find comprehensive benchmarks notably comparing all heuristics to build idealisation here.

References

[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. To appear. A copy can be found at http://projects.lsv.ens-cachan.fr/ukano/.

[H17]: L. Hirschi. PhD Thesis. Automated Verification of Privacy in Security Protocols: Back and Forth Between Theory & Practice. A copy will soon be distributed at http://projects.lsv.ens-cachan.fr/ukano/.

[BFK-09]: J. Bender, M. Fischlin, and D. Kügler. Security analysis of the pace key-agreement protocol. In Information Security, pages 33–48. Springer, 2009.

Table of Contents

Clone this wiki locally