Looping for Good: Cyclic Proofs for Security Protocols

This work introduces reasoning rules for the Tamarin prover for cyclic proofs, enabling new, compact proofs, and proves their soundness, and implements new, simple, and effective proof search strategies that leverage these rules.