Automated Verification of Equivalence Properties of Cryptographic Protocols
From MaRDI portal
Publication:5278194
DOI10.1145/2926715zbMath1367.68184OpenAlexW2521663436MaRDI QIDQ5278194
Ştefan Ciobâcă, Steve Kremer, Vincent Cheval, Rohit Chadha
Publication date: 13 July 2017
Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/2926715
Related Items
When privacy fails, a formula describes an attack: a complete and compositional verification method for the applied \(\pi\)-calculus ⋮ An efficient canonical narrowing implementation with irreducibility and SMT constraints for generic symbolic protocol analysis ⋮ Security Protocol Analysis in Context: Computing Minimal Executions Using SMT and CPSA ⋮ Computing knowledge in equational extensions of subterm convergent theories ⋮ Beyond Subterm-Convergent Equational Theories in Automated Verification of Stateful Protocols ⋮ On Communication Models When Verifying Equivalence Properties ⋮ A survey of symbolic methods for establishing equivalence-based properties in cryptographic protocols ⋮ Unnamed Item ⋮ Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Decidability of equivalence of symbolic derivations
- Computing knowledge in security protocols under convergent equational theories
- Deciding \(\mathcal H_1\) by resolution
- A calculus for cryptographic protocols: The spi calculus
- Private authentication
- Folding variant narrowing and optimal variant termination
- Automated Verification of Equivalence Properties of Cryptographic Protocols
- Formal Analysis of Privacy for Anonymous Location Based Services
- Simulation based security in the applied pi calculus
- Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties
- A Complete Symbolic Bisimulation for Full Applied Pi Calculus
- Deciding Knowledge in Security Protocols for Monoidal Equational Theories
- Combining Algorithms for Deciding Knowledge in Security Protocols
- A Framework for Automatically Checking Anonymity with μCRL
- Verification of Security Protocols with a Bounded Number of Sessions Based on Resolution for Rigid Variables
- YAPA: A Generic Tool for Computing Intruder Knowledge
- A practical secret voting scheme for large scale elections
- On the unification problem for Cartesian closed categories
- Term Rewriting and All That
- Mobile values, new names, and secure communication
- Computing Knowledge in Security Protocols under Convergent Equational Theories
- CONCUR 2004 - Concurrency Theory
- Programming Languages and Systems
- Practical Everlasting Privacy
- Proving More Observational Equivalences with ProVerif
- Intruders with Caps
- Term Rewriting and Applications
- Automating Security Analysis: Symbolic Equivalence of Constraint Systems
