Skip to main content

Trace Equivalence Decision: Negative Tests and Non-determinism

Cheval, Vincent and Comon-Lundh, Hubert and Delaune, Stéphanie (2011) Trace Equivalence Decision: Negative Tests and Non-determinism. In: Chen, Yan and Danezis, George and Shmatikov, Vitaly, eds. Proceedings of the 18th ACM conference on Computer and communications security. ACM, New York, USA, pp. 321-330. ISBN 978-1-4503-0948-6. (doi:10.1145/2046707.2046744) (KAR id:46878)

PDF Publisher pdf
Language: English
Download (236kB) Preview
[thumbnail of CCD-ccs11.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 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: Book section
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: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Vincent Cheval
Date Deposited: 23 Jan 2015 11:49 UTC
Last Modified: 16 Nov 2021 10:19 UTC
Resource URI: (The current URI for this page, for reference purposes)
  • Depositors only (login required):


Downloads per month over past year