These are Tamarin models submitted for review.
The Tamarin files in the folder called "diff" are models where we used diff-equivalence.
Contrary to this, the Tamarin files in the folder called "indist" use the trace-based lemmas to disprove privacy in AKMA, and exhibit explicit tracking.
In the folder called "correctness", we have Tamarin files proving correctness, or general functionality for the entire of the 3GPP specification or our adaption of it to AKMAP, and it is not a model focused privacy (which is just for sanity checks and not essential to this paper).
Tamarin files (.spthy) that contain the sequence of letters "_AKMA_" are models of the AKMA protocol.
Tamarin files that ontain the sequence of letters "_AKMAP_" are models the protocol we call AKMAP, which is a version of AKMA with provable privacy guarantees, that is also backwards-compatible with the current AKMA specifications by 3GPP (i.e., we do not add new messages, or new cryptography, etc;).
The names of the files are as per Table 2 (for AKMA) and Table 3 (for AKMAP), in the paper. That is, the names of the Tamarin files generally start with the privacy property in the paper that we prove in that file (e.g., PP, SS, WP, Unlink).
If a Tamarin file starts directly with "AKMA" or "AKMAP", then it is a file proving correctness rather than privacy.
We also provide oracles in some cases (.oracle). The names of these are telling, as to which .spthy files they go with. In any case, the oracles are already included in the .spthy files where they are needed.
We use Tamarin 1.6.1 for some of our proofs, and Tamarin 1.8 for others. This is purely based on the fact that Tamarin 1.8 is slower for our diff-equivalence proofs. Our models work in both Tamarin versions.
For running each file, you will find a comment inside its headers: e.g., "tamarin-prover-161 WP_AKMA.spthy --prove && date". This may be for Tamarin 1.6 or Tamarin 1.8, but it will be clear from the command.