Deciding equivalence-based properties using constraint solving

DOI10.1016/j.tcs.2013.04.016zbMath1294.68111OpenAlexW2005880313MaRDI QIDQ391121

Véronique Cortier, Vincent Cheval, Stéphanie Delaune

Publication date: 10 January 2014

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2013.04.016

zbMATH Keywords

formal verificationsecurity protocolsapplied-pi calculusbehavioral equivalencesconstraint systems

Mathematics Subject Classification ID

Cryptography (94A60) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Network protocols (68M12)

Related Items (8)

Trace Equivalence and Epistemic Logic to Express Security Properties ⋮ Stateful applied pi calculus: observational equivalence and labelled bisimilarity ⋮ POR for security protocol equivalences. Beyond action-determinism ⋮ Efficiently deciding equivalence for standard primitives and phases ⋮ On the existence and decidability of unique decompositions of processes in the applied \(\pi\)-calculus ⋮ On Communication Models When Verifying Equivalence Properties ⋮ A survey of symbolic methods for establishing equivalence-based properties in cryptographic protocols ⋮ A procedure for deciding symbolic equivalence between sets of constraint systems

Uses Software

• AVISPA
• scyther
• ConfiChair
• Akiss

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Decidability of equivalence of symbolic derivations
• Deciding knowledge in security protocols under equational theories
• Determinacy \(\to\) (observation equivalence \(=\) trace equivalence)
• A calculus of communicating systems
• Testing equivalences for processes
• On the symbolic reduction of processes with cryptographic functions.
• Private authentication
• Automated verification of selected equivalences for security protocols
• Hierarchical combination of intruder theories
• Proof Techniques for Cryptographic Processes
• Automated Verification of Equivalence Properties of Cryptographic Protocols
• Proof System for Applied Pi Calculus
• A Complete Symbolic Bisimulation for Full Applied Pi Calculus
• Communicating sequential processes
• Mobile values, new names, and secure communication
• FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science
• Proving More Observational Equivalences with ProVerif
• Symbolic Bisimulation for the Applied Pi Calculus
• Computer Aided Verification

This page was built for publication: Deciding equivalence-based properties using constraint solving