Sciweavers

CADE
2010
Springer

Automating Security Analysis: Symbolic Equivalence of Constraint Systems

13 years 4 months ago
Automating Security Analysis: Symbolic Equivalence of Constraint Systems
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.
Vincent Cheval, Hubert Comon-Lundh, Stéphan
Added 08 Nov 2010
Updated 08 Nov 2010
Type Conference
Year 2010
Where CADE
Authors Vincent Cheval, Hubert Comon-Lundh, Stéphanie Delaune
Comments (0)