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 - CCS '11. ACM Press pp. 321-330. ISBN 978-1-4503-0948-6. (doi:https://doi.org/10.1145/2046707.2046744) (Full text available)

PDF - Publisher pdf
Download (236kB) Preview
[img]
Preview
Official URL
http://dx.doi.org/10.1145/2046707.2046744

Abstract

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)
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: 23 Jan 2015 11:49 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/46878 (The current URI for this page, for reference purposes)
  • Depositors only (login required):

Downloads

Downloads per month over past year