Skip to content

festutz/eID-protocol-models

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

1 Commit
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

eID Protocol Models

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.

Reproducing Results

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

About

No description, website, or topics provided.

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published