Comparing State Spaces in Automatic Security Protocol Analysis

DOI10.1007/978-3-642-02002-5_5MaRDI QIDQ3631370zbMATH OpenOpenAlexFDO

Authors Pascal Lafourcade, Philippe Nadeau, C. J. F. Cremers

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_5

Mathematics Subject Classification ID

Data encryption (aspects in computer science) (68P25) Cryptography (94A60)

Recommendations

• State space reduction in the Maude-NRL protocol analyzer
• scientific article; zbMATH DE number 1927581
• Cryptographic protocol security analysis based on bounded constructing algorithm
• Trustworthy Global Computing
• The CL-Atse Protocol Analyser

Cites work

• A logic of authentication
• An Obvious Proof of Burnside's Lemma
• An optimized intruder model for SAT-based model-checking of security protocols
• Applied finite group actions.
• Computer Aided Verification
• scientific article; zbMATH DE number 4039251 (Why is no real title available?)
• scientific article; zbMATH DE number 1948405 (Why is no real title available?)
• scientific article; zbMATH DE number 1962758 (Why is no real title available?)
• scientific article; zbMATH DE number 1927582 (Why is no real title available?)
• scientific article; zbMATH DE number 1754628 (Why is no real title available?)
• scientific article; zbMATH DE number 3443655 (Why is no real title available?)
• scientific article; zbMATH DE number 1903364 (Why is no real title available?)
• Injective synchronisation: An extension of the authentication hierarchy
• Security properties: two agents are sufficient
• The CL-Atse Protocol Analyser
• Using encryption for authentication in large networks of computers

Cited in

(4)

• Cross-tool semantics for protocol security goals
• Formal analysis and offline monitoring of electronic exams
• State space reduction in the Maude-NRL protocol analyzer
• Tree automata for detecting attacks on protocols with algebraic cryptographic primitives

Describes a project that uses

Uses Software

• HERMES
• Casper
• AVISPA
• scyther

This page was built for publication: Comparing State Spaces in Automatic Security Protocol Analysis

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