Automating Security Analysis: Symbolic Equivalence of Constraint Systems

Cheval, Vincent, Comon-Lundh, Hubert, Delaune, Stéphanie (2010) Automating Security Analysis: Symbolic Equivalence of Constraint Systems. In: Giesl, Jürgen and Hähnle, Reiner, eds. Proceedings of the 5th International Joint Conference on Automated Reasoning (IJCAR'10). Lecture Notes in Computer Science , 6173. pp. 412-426. Springer-Verlag Berlin, Edinburgh, Scotland, UK ISBN 978-3-642-14202-4. E-ISBN 978-3-642-14203-1. (doi:10.1007/978-3-642-14203-1_35)


We consider security properties of cryptographic protocols, that are either trace properties (such as confidentiality or authenticity) or equivalence properties (such as anonymity or strong secrecy). Infinite sets of possible traces are symbolically represented using deducibility constraints. We give a new algorithm that decides the trace equivalence for the traces that are represented using such constraints, in the case of signatures, symmetric and asymmetric encryptions. Our algorithm is implemented and performs well on typical benchmarks. This is the first implemented algorithm, deciding symbolic trace equivalence.

Item Type: Conference or workshop item (Paper)
DOI/Identification number: 10.1007/978-3-642-14203-1_35
Uncontrolled keywords: Cryptographic protocols, Formal verification, Symbolic model, Automatic, Equivalence properties, Constraint systems
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 75 Electronic computers. Computer science
Q Science > QA Mathematics (inc Computing science) > QA 9 Formal systems, logics
Divisions: Faculties > Sciences > School of Computing > Security Group
Depositing User: Vincent Cheval
Date Deposited: 20 Jan 2015 11:30 UTC
Last Modified: 29 May 2019 14:05 UTC
Resource URI: (The current URI for this page, for reference purposes)
  • Depositors only (login required):


Downloads per month over past year