Verification of cryptographic protocols: tagging enforces termination

DOI10.1016/j.tcs.2004.10.018zbMath1070.68033OpenAlexW2097134979MaRDI QIDQ1770413

Bruno Blanchet, Andreas Podelski

Publication date: 6 April 2005

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2004.10.018

zbMATH Keywords

Horn clausesTerminationResolutionCryptographic protocolsTagging

Mathematics Subject Classification ID

Data encryption (aspects in computer science) (68P25)

Related Items (7)

Causality, Behavioural Equivalences, and the Security of Cyberphysical Systems ⋮ Challenges in the Automated Verification of Security Protocols ⋮ Bounding messages for free in security protocols -- extension to various security properties ⋮ Automated type-based analysis of injective agreement in the presence of compromised principals ⋮ Unnamed Item ⋮ Bounding Messages for Free in Security Protocols ⋮ Automatic Verification of Security Protocols in the Symbolic Model: The Verifier ProVerif

Uses Software

• TAPS

Cites Work

• Computer security -- ESORICS 2000. 6th European symposium on research in computer security, Toulouse, France, October 4--6, 2000. Proceedings
• Using encryption for authentication in large networks of computers
• A logic of authentication
• Analyzing security protocols with secrecy types and logic programs
• FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Verification of cryptographic protocols: tagging enforces termination