Looping for Good: Cyclic Proofs for Security Protocols

Security protocols often involve loops, such as for ratcheting or for manipulating inductively-defined data structures. However, the automated analysis of security protocols has struggled to keep up with these features. The state-of-the-art often necessitates working with abstractions of such data structures or relies heavily on auxiliary, user-defined lemmas.