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 this file (PDF/259kB)	Preview
Request a format suitable for use with assistive technology e.g. a screenreader
Official URL: http://dx.doi.org/10.1007/978-3-642-14203-1_35

Abstract

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:	https://kar.kent.ac.uk/id/eprint/46730 (The current URI for this page, for reference purposes)

University of Kent Author Information

Cheval, Vincent.

Creator's ORCID:
CReDIT Contributor Roles:

Depositors only (login required):

Altmetric

Download Statistics

Total unique views for this document in KAR since July 2020. For more details click on the image.