Trace Equivalence Decision: Negative Tests and Non-determinism

Cheval, Vincent, Comon-Lundh, Hubert, Delaune, Stéphanie (2011) Trace Equivalence Decision: Negative Tests and Non-determinism. In: 18th ACM Conference on Computer and Communications Security (CCS'11), October 2011, Chicago, Illinois, USA. (doi:10.1145/2046707.2046744)

PDF - Publisher pdf
Download (236kB) Preview
Official URL


We consider security properties of cryptographic protocols that can be modeled using the notion of trace equivalence. The notion of equivalence is crucial when specifying privacy-type properties, like anonymity, vote-privacy, and unlinkability. In this paper, we give a calculus that is close to the applied pi calculus and that allows one to capture most existing protocols that rely on classical cryptographic primitives. First, we propose a symbolic semantics for our calculus relying on constraint systems to represent infinite sets of possible traces, and we reduce the decidability of trace equivalence to deciding a notion of symbolic equivalence between sets of constraint systems. Second, we develop an algorithm allowing us to decide whether two sets of constraint systems are in symbolic equivalence or not. Altogether, this yields the first decidability result of trace equivalence for a general class of processes that may involve else branches and/or private channels (for a bounded number of sessions).

Item Type: Conference or workshop item (Paper)
DOI/Identification number: 10.1145/2046707.2046744
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: 23 Jan 2015 11:49 UTC
Last Modified: 29 May 2019 14:08 UTC
Resource URI: (The current URI for this page, for reference purposes)
  • Depositors only (login required):


Downloads per month over past year