This project contains the different versions of EAC from https://ia.cr/2023/352.
This project was created as part of the master thesis "EAC Analysis in Tamarin Prover" at the TU Darmstadt. It contains the different versions of EAC from https://ia.cr/2023/352.
The models are the classic EAC, SigPQEAC and KemPQEAC as well as the forward seccrecy and saved round-trip modifications.
The models are the classic EAC, SigPQEAC and KemPQEAC as well as the forward seccrecy and saved round-trip modifications.
The [python script](InsertLemmas.py) inserts the different sections into the .spthy files and creates the tmp.spthy file. Usage: python InsertLemmas.py file.spthy
The [python script](InsertLemmas.py) inserts the different sections into the .spthy files and creates the tmp.spthy file. Usage: python InsertLemmas.py file.spthy
The [include](include/) directory contains the code that will be included to the different models.
The [include](include/) directory contains the code that will be included to the different models.