This repository contains different models of 4 eID protocols that specify different corruption and user mistake scenarios. Tamarin can be used to automatically check which security level can still be achieved in such scenarios. This accompanies work-in-progress by Ole Martin Edstrøm, Kristian Gjøsteen, Hans Heum, Sjouke Mauw, and Felix Stutz. We plan to provide a link to a technical report soon.
We used Tamarin to analyse these models on a laptop (with an Apple M2 Pro chip with 16 BG of memory and 10 cores), using Tamarin (Version 1.10.0) and Maude (Version 2.7.1).
One can use the following command, e.g. for Password:
tamarin-prover --quit-on-warning --prove Password.spthy > Password.result
For each model, we provide the result we obtained in the folder results
.
For reference, the time and memory usage for each model can be found below.
As reported by the command /usr/bin/time -l
(-l
is an option for BSD versions while -v
provides similar output for GNU versions):
Password.spthy 45.53 real 111.43 user 9.36 sys 298583744 peak memory footprint
AppOnly.spthy 55.70 real 109.96 user 11.93 sys 705464768 peak memory footprint
AppOnly_Plus.spthy 56.35 real 112.29 user 12.10 sys 719178240 peak memory footprint
AppOnlyWrite.spthy 45.99 real 94.32 user 9.75 sys 591218944 peak memory footprint
AppOnlyWrite_Plus.spthy 46.60 real 93.95 user 9.89 sys 596428992 peak memory footprint
AppOnlyCompare.spthy 60.89 real 118.68 user 12.81 sys 718260736 peak memory footprint
AppOnlyCompare_Plus.spthy 62.29 real 126.02 user 13.79 sys 752880192 peak memory footprint
WebAuthn.spthy 432.21 real 889.08 user 88.51 sys 521996288 peak memory footprint
WebAuthn_Plus.spthy 426.93 real 882.99 user 87.34 sys 519850112 peak memory footprint
TwoFactor.spthy 7998.48 real 13909.54 user 1540.29 sys 1639321728 peak memory footprint
TwoFactor_Plus.spthy 8030.49 real 13951.73 user 1577.65 sys 1673974016 peak memory footprint
TwoFactorWrite.spthy 2914.31 real 5022.81 user 568.99 sys 1175637376 peak memory footprint
TwoFactorWrite_Plus.spthy 2956.33 real 5017.58 user 556.35 sys 1196592448 peak memory footprint
TwoFactorWriteCompare.spthy 8269.27 real 14465.76 user 1613.75 sys 1670910208 peak memory footprint
TwoFactorWriteCompare_Plus.spthy 8294.73 real 14474.73 user 1590.00 sys 1672941824 peak memory footprint
As reported by Tamarin:
Password.result: processing time: 45.47s
AppOnly.result: processing time: 55.65s
AppOnly_Plus.result: processing time: 56.28s
AppOnlyWrite.result: processing time: 45.93s
AppOnlyWrite_Plus.result: processing time: 46.54s
AppOnlyCompare.result: processing time: 60.82s
AppOnlyCompare_Plus.result: processing time: 62.22s
TwoFactor.result: processing time: 7998.41s
TwoFactor_Plus.result: processing time: 8030.40s
TwoFactorWrite.result: processing time: 2914.24s
TwoFactorWrite_Plus.result: processing time: 2956.26s
TwoFactorWriteCompare.result: processing time: 8269.19s
TwoFactorWriteCompare_Plus.result: processing time: 8294.57s
WebAuthn.result: processing time: 432.16s
WebAuthn_Plus.result: processing time: 426.87s