A decidable class of security protocols for both reachability and equivalence properties

DOI10.1007/s10817-020-09582-9OpenAlexW3003059772MaRDI QIDQ2031426

Stéphanie Delaune, Véronique Cortier, Vaishnavi Sundararajan

Publication date: 9 June 2021

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://hal.inria.fr/hal-03005036/file/main.pdf

zbMATH Keywords

verificationsecurity protocolsprivacy properties

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Uses Software

• AVISPA
• Akiss
• TAMARIN

Cites Work

• Unnamed Item
• Unnamed Item
• Principles of security and trust. 5th international conference, POST 2016, held as part of the European joint conferences on theory and practice of software, ETAPS 2016, Eindhoven, The Netherlands, April 2--8, 2016. Proceedings
• A survey of symbolic methods for establishing equivalence-based properties in cryptographic protocols
• A rewriting-based inference system for the NRL protocol analyzer and its meta-logical properties
• A calculus for cryptographic protocols: The spi calculus
• Protocol insecurity with a finite number of sessions and composed keys is NP-complete.
• Efficiently deciding equivalence for standard primitives and phases
• Automated Verification of Equivalence Properties of Cryptographic Protocols
• Typing Messages for Free in Security Protocols: The Case of Equivalence Properties
• Typing Messages for Free in Security Protocols
• Mobile values, new names, and secure communication
• FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science
• From Security Protocols to Pushdown Automata
• Computer Aided Verification