This directory contains the verified Proof for the SAPIC representation of the
Yubikey protocol. As SAPIC's translation and tamarin's constraint solving
algorithm change from time to time, it is difficult to maintain the proof.
Hence, for reproducibility, this directory contains the current file (which
cannot be verified automatically, just like the original proof needed some
guidance) as well as the files that were discussed in the paper.


It contains:

Yubikey.spthy              -- SAPIC file compatible with the process translation implemented in tamarin-sapic
Yubikey_reference.apip     -- original SAPIC file, at that time called apip (applied-pi-like protocol)
model_used_in_proofs.spthy -- The translation of the previous file into msr rules
proof_manual_part.spthy    -- The manual part of the proof
proof_complete.spthy       -- The complete proof
