On Communication Models When Verifying Equivalence Properties

DOI10.1007/978-3-662-54455-6_7MaRDI QIDQ3304813zbMATH OpenOpenAlexFDO

Authors Kushal Babel, Vincent Cheval, Steve Kremer

Publication date 3 August 2020

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

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

zbMATH Keywords

operational semanticsauthentication protocolclassical semanticsextended process

Mathematics Subject Classification ID

Cryptography (94A60) Specification and verification (program logics, model checking, etc.) (68Q60) Semantics in the theory of computing (68Q55) Authentication, digital signatures and secret sharing (94A62) Network protocols (68M12) Computer security (68M25)

Recommendations

• A survey of symbolic methods for establishing equivalence-based properties in cryptographic protocols
• On the relationships between models in protocol verification
• About models of security protocols
• Verification methods for the computationally complete symbolic attacker based on indistinguishability
• Towards unconditional soundness: computationally complete symbolic attacker

Cites work

• A calculus for cryptographic protocols: The spi calculus
• Automated verification of equivalence properties of cryptographic protocols
• Automated verification of selected equivalences for security protocols
• Automating security analysis: symbolic equivalence of constraint systems
• Computer Aided Verification
• Deciding equivalence-based properties using constraint solving
• Mobile values, new names, and secure communication
• Private authentication
• Verifying privacy-type properties of electronic voting protocols: a taster

Cited in

(3)

• Verification methods for the computationally complete symbolic attacker based on indistinguishability
• On the relationships between models in protocol verification
• Type-Based Verification of Correspondence Assertions for Communication Protocols

Describes a project that uses

Uses Software

• TAMARIN
• Akiss
• Apte
• AVISPA

This page was built for publication: On Communication Models When Verifying Equivalence Properties

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