Skip to main content

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) (KAR id:46730)

PDF Publisher pdf
Language: English
Download (229kB) Preview
[thumbnail of CCD-ijcar10.pdf]
This file may not be suitable for users of assistive technology.
Request an accessible format
Official URL


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: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Vincent Cheval
Date Deposited: 20 Jan 2015 11:30 UTC
Last Modified: 16 Nov 2021 10:18 UTC
Resource URI: (The current URI for this page, for reference purposes)
  • Depositors only (login required):