ProVerif Models for Verifying Unlinkability of EAP-SIM and EAP-AKA

The archive containing the models and a README explaining the role of each file can be found here.

You need ProVerif version >1.96 . To run a model, type:

proverif -in pitype <filename>