Bridging Theory and Practice: An Executable Taxonomy of Security Properties for ProVerif and Tamarin

Computer Science > Cryptography and Security [Submitted on 28 May 2026] Bridging Theory and Practice: An Executable Taxonomy of Security Properties for ProVerif and Tamarin Leonard Tudorache, Ivan Kurtev, Mark van den Brand Security is critical for everything relying on modern digital systems. Because almost all digital interactions are governed by the Internet and cryptographic protocols, these protocols must serve as reliable mechanisms that guarantee core security properties, such as confidentiality and integrity. Formal verification of these protocols is a critical step in securing interconnected systems. Tools such as ProVerif and Tamarin are widely employed to perform automated verification. However, their effective use demands specialized domain knowledge, creating a significant learning curve for security protocol designers who often have a security, rather than a formal verification background. We therefore need structured, accessible resources to help protocol designers to express their design and requirements in the language of the formal verification tools. To address this, we introduce a systematic and evidence-based taxonomy of security properties. This taxonomy is derived from a literature review of 53 recent studies (2022-2025) that used ProVerif and Tamarin, providing an up-to-date view of verified properties. We systematically categorize and define these properties, providing both informal definitions for intuitive comprehension and rigorous formal definitions expressed in first-order logic for clarity and consistency. We further detail modeling patterns and implement executable examples in both ProVerif and Tamarin, collected in an open repository. This work advances the state of the art by bridging the gap between theoretical security property definitions and their practical, executable verification models. Comments: Under review at International Journal on Software and Systems Modeling (SoSyM) Subjects: Cryptography and Security (cs.CR) Cite as: arXiv:2605.29465 [cs.CR]   (or arXiv:2605.29465v1 [cs.CR] for this version)   https://doi.org/10.48550/arXiv.2605.29465 Focus to learn more Submission history From: Leonard Tudorache [view email] [v1] Thu, 28 May 2026 06:57:08 UTC (1,191 KB) Access Paper: HTML (experimental) view license Current browse context: cs.CR < prev   |   next > new | recent | 2026-05 Change to browse by: cs References & Citations NASA ADS Google Scholar Semantic Scholar Export BibTeX Citation Bookmark Bibliographic Tools Bibliographic and Citation Tools Bibliographic Explorer Toggle Bibliographic Explorer (What is the Explorer?) Connected Papers Toggle Connected Papers (What is Connected Papers?) Litmaps Toggle Litmaps (What is Litmaps?) scite.ai Toggle scite Smart Citations (What are Smart Citations?) Code, Data, Media Demos Related Papers About arXivLabs Which authors of this paper are endorsers? | Disable MathJax (What is MathJax?)