Looping for Good: Cyclic Proofs for Security Protocols
Loading...
Author / Producer
Date
2025-11-22
Publication Type
Conference Paper
ETH Bibliography
yes
Citations
Altmetric
Data
Rights / License
Abstract
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
Permanent link
Publication status
published
External links
Editor
Book title
CCS '25: Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security
Journal / series
Volume
Pages / Article No.
2759 - 2773
Publisher
Association for Computing Machinery
Event
32nd ACM Conference on Computer and Communications Security (CCS)
Edition / version
Methods
Software
Geographic location
Date collected
Date created
Subject
Security protocol verification; Formal methods; Cyclic induction; Tamarin prover
Organisational unit
03634 - Basin, David / Basin, David