We have tested UKano on several real-world case studies.
This folder contains all ProVerif models for which unlinkability
and anonymity can be automatically established using UKano.
They all have a dedicatd folder in ./examples/.
We list them all in the next section and provide benchmarks in section Benchmarks.
Finally, note that for some protocols, you need to use specific idealisation heuristics as explained in the dedicated section of the wiki. We also list in section Benchmarks the different results (conclusion and time needed to conclude) one obtains depending on the chosen heuristic.
Remark that, in some files, we may use multiple conditionals in a row to ease the readability.
Note that UKano considers them as a single compacted conditional. We also show how
UKano detects some attacks on variations of protocols that do not satisfy our conditions
(corresponding files end with -attack.pi).
Finally, the folder ./examples/tamarin/ contains
some Tamarin models mentioned in [H17]; they are obviously not valid
UKano files.
See the table below. References to the protocols can be found at [HBD17].
Legend:
- ✅ : means that the corresponding condition or property could be automaticaly 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) | ✅ | ✅ | ✅ |
All benchmarks are performed using UKano v0.2 (with ProVerif v1.92 as backend) without user-defined idealisations (except for some cases indicated with (*)). For most cases, the verification is thus truly fully automatic.
Here are the specs of the machine we used: We performed those benchmarks on this machine:
- OS: Linux sume 3.10-2-amd64 #1 SMP Debian 3.10.5-1 (2013-08-07) x86_64 GNU/Linux
- CPU: Intel(R) Xeon(R) CPU X5650 @ 2.67GHz / stepping: 2 / microcode: 0x13 / cpu MHz: 2659.937 / cache size: 12288 KB
- RAM: 47GO
Legend: time in seconds when verification was successful, ❌ when condition could not be established, ➰ when the verification took too much time (>20 hours) or too much memory (>20GO of RAM), and, -- when it was not necessary to build idealisations manually (i.e., user defined). The different columns for FO (i.e., frame opacity) refers to the different heuristics implemented in UKano to build idealisations:
- "greedy" corresponds to the option
--ideal-greedy - "default" corresponds to the default heuristic of UKano
- "syntax" corresponds to the option
--ideal-full-syntax - "user-defined" when a user-defined idealisation is necessary
| Protocol | Better time (total) | Time for WA | Time for FO (greedy) | Time for FO (default) | Time for FO (syntax) | Time for FO (user-defined) |
|---|---|---|---|---|---|---|
| Hash-Lock | 0.00s | 0.00s | 0.00s | 0.00s | 0.00s | -- |
| Fixed LAK | 0.00s | 0.00s | 0.00s | 0.00s | 0.00s | -- |
| BAC | 8.41s | 0.02s | 8.39s | 17.24s | 17.20s | -- |
| BAC+AA+PA | 198.28s | 0.42s | 197.86s | 1013.56s | 998.81s | -- |
| BAC+PA+AA | 183.40s | 0.33s | 183.07s | 1068.79s | 1191.04s | -- |
| PACE with tags | 169.91 | 62.99s | 106.92s (*) | ➰ | ➰ | 106.92s |
| DAA simplified [HBD17] | 0.02s | 0.01s | ❌ | 0.01s | 0.00s | -- |
| DAA sign | 2.94s | 0.01s | ❌ | ❌ | 2.76s | -- |
| DAA join | 4.68s | 1.82s | 2.30s | 2.30s | 28.85s | -- |
| abcdh (irma) | 8479.76 | 9060 | ❌ | ❌ | 2389.76s* | 2389.76s |
(*) indicates that we had to slightly modify the produced file.
We also report on the table below the time needed to find an attack (on well-authentication):
| Protocol | Time to find an attack in WA |
|---|---|
| PACE (faillible dec) | 31.81s |
| PACE (as in BFK-09) | 61.43s |
| PACE | 83.72s |
[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.