Alice and Bob meet equational theories

DOI10.1007/978-3-319-23165-5_7MaRDI QIDQ2945705zbMATH OpenOpenAlexFDO

Authors Michel Keller, Saša Radomirović, Ralf Sasse, David Basin

Publication date 14 September 2015

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-23165-5_7

Mathematics Subject Classification ID

Cryptography (94A60) Specification and verification (program logics, model checking, etc.) (68Q60) Network protocols (68M12)

Recommendations

• Alice and Bob: reconciling formal models and implementation
• Cryptographic protocol security analysis based on bounded constructing algorithm
• Three systems for cryptographic protocol analysis
• scientific article; zbMATH DE number 1405638
• Algebraic Intruder Deductions

Cites work

• Alice and Bob meet equational theories
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• Compiling and securing cryptographic protocols
• Computer Aided Verification
• Cryptographic Protocol Explication and End-Point Projection
• Deconstructing Alice and Bob
• Folding variant narrowing and optimal variant termination
• Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties
• On the semantics of Alice \& Bob specifications of security protocols
• Provably repairing the ISO/IEC 9798 standard for entity authentication
• Term Rewriting and All That
• Term Rewriting and Applications

Cited in

(8)

• Introducing commutative and associative operators in cryptographic protocol analysis
• Alice and Bob meet equational theories
• On the semantics of Alice \& Bob specifications of security protocols
• Alice and Bob: reconciling formal models and implementation
• Optimization of ProVerif Programs for AKE Protocols
• Deconstructing Alice and Bob
• scientific article; zbMATH DE number 1956542 (Why is no real title available?)
• G2C: cryptographic protocols from goal-driven specifications

Describes a project that uses

Uses Software

• GitHub
• TAMARIN
• scyther-proof
• Casper
• ProVerif
• Maude
• AVISPA

This page was built for publication: Alice and Bob meet equational theories

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