Verification of Security Protocols with a Bounded Number of Sessions Based on Resolution for Rigid Variables

DOI10.1007/978-3-642-02002-5_1MaRDI QIDQ3631368zbMATH OpenOpenAlexFDO

Authors Reynald Affeldt, Hubert Comon-Lundh

Publication date 9 June 2009

Published in Formal to Practical Security (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-02002-5_1

Mathematics Subject Classification ID

Cryptography (94A60) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)

Recommendations

• Protocol Security and Algebraic Properties: Decision Results for a Bounded Number of Sessions
• scientific article; zbMATH DE number 7559487
• scientific article; zbMATH DE number 1948405
• scientific article; zbMATH DE number 7650814
• scientific article; zbMATH DE number 7297874
• Protocol Verification Via Rigid/Flexible Resolution
• Constraint Abstraction in Verification of Security Protocols
• A coordination-based methodology for security protocol verification

Cites work

• scientific article; zbMATH DE number 1341618 (Why is no real title available?)
• scientific article; zbMATH DE number 1962758 (Why is no real title available?)
• An NP decision procedure for protocol insecurity with XOR
• Deciding security properties for cryptographic protocols. application to key cycles
• Programming Languages and Systems
• Protocol Verification Via Rigid/Flexible Resolution
• Protocol insecurity with a finite number of sessions and composed keys is NP-complete.
• Resolution decision procedures
• Resolution theorem proving
• Security properties: two agents are sufficient
• Theorem Proving via General Matings

Cited in

(6)

• Protocol insecurity with a finite number of sessions and a cost-sensitive guessing intruder is NP-complete
• A (restricted) quantifier elimination for security protocols
• Challenges in the Automated Verification of Security Protocols
• Automated verification of equivalence properties of cryptographic protocols
• Rigid tree automata and applications
• Protocol Verification Via Rigid/Flexible Resolution

This page was built for publication: Verification of Security Protocols with a Bounded Number of Sessions Based on Resolution for Rigid Variables

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3631368)