Looping for Good: Cyclic Proofs for Security Protocols

Zusammenfassung

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. In this work, we advance the state-of-the-art in symbolic protocol verification by adapting cyclic induction proof systems to the security protocol domain. We introduce reasoning rules for the Tamarin prover for cyclic proofs, enabling new, compact proofs, and we prove their soundness. Moreover, we implement new, simple, and effective proof search strategies that leverage these rules. With these additions, Tamarin can prove many lemmas that previously required, often complex, auxiliary lemmas. We showcase our approach on fourteen case studies, ranging from toy examples to a detailed model of the Signal protocol. Our work opens an exciting new research area where automatic induction helps scale security protocol verification, as we provide a fundamentally new and general induction mechanism.