Beyond Subterm-Convergent Equational Theories in Automated Verification of Stateful Protocols

DOI10.1007/978-3-662-54455-6_6zbMath1444.68040OpenAlexW2584482469MaRDI QIDQ3304811

Charles Duménil, Jannik Dreier, Ralf Sasse, 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-01430490/file/techreport.pdf

zbMATH Keywords

dependency graphequational theoryblind signaturebilinear pairingconstruction rule

Mathematics Subject Classification ID

Cryptography (94A60) Specification and verification (program logics, model checking, etc.) (68Q60) Computer security (68M25)

Related Items (4)

Modular verification of protocol equivalence in the presence of randomness ⋮ Automated identification of desynchronisation attacks on shared secrets ⋮ Unnamed Item ⋮ Programming and symbolic computation in Maude

Uses Software

• AVISPA
• Maude-NPA
• Akiss
• TAMARIN
• CPSA
• Helios

Cites Work

• Unnamed Item
• Folding variant narrowing and optimal variant termination
• Automated verification of selected equivalences for security protocols
• Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties
• Coercion-Resistant Electronic Elections
• Verifying Privacy-Type Properties of Electronic Voting Protocols: A Taster
• A practical secret voting scheme for large scale elections
• Automated Verification of Equivalence Properties of Cryptographic Protocols
• Intruders with Caps
• Term Rewriting and Applications
• Computer Aided Verification
• Automating Security Analysis: Symbolic Equivalence of Constraint Systems

This page was built for publication: Beyond Subterm-Convergent Equational Theories in Automated Verification of Stateful Protocols