A (work-in-progress) implementation of IPsec in Tamarin-Prover for automated security analysis
- Tamarin-Prover v1.2.3. or later
- m4 v1.4.18 or later
The code is spread over several files using m4. One can compile a complete theory file for Tamarin-Prover by running
$ m4 ipsec.m4 Once the security protocol theory is compiled from the previous step, you may execute the following command to run the security analysis:
$ tamarin-prover --prove ipsec.spthy