A procedure for deciding symbolic equivalence between sets of constraint systems

Cheval, Vincent and Comon-Lundh, Hubert and Delaune, Stéphanie (2017) A procedure for deciding symbolic equivalence between sets of constraint systems. Information and Computation, 255 (part 1). pp. 94-125. ISSN 0890-5401. E-ISSN 1090-2651. (doi:https://doi.org/10.1016/j.ic.2017.05.004) (Access to this publication is currently restricted. You may be able to access a copy if URLs are provided)

PDF - Author's Accepted Manuscript
Restricted to Repository staff only until 31 May 2019.

Creative Commons Licence
This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.
Contact us about this Publication Download (490kB)
[img]
Official URL
http://dx.doi.org/10.1016/j.ic.2017.05.004

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. Infinite sets of possible traces are symbolically represented using deducibility constraints. We describe an algorithm that decides trace equivalence for protocols that use standard primitives (e.g., signatures, symmetric and asymmetric encryptions) and that can be represented using such constraints. More precisely, we consider symbolic equivalence between sets of constraint systems, and we also consider disequations. Considering sets and disequations is actually crucial to decide trace equivalence for a general class of processes that may involve else branches and/or private channels (for a bounded number of sessions). Our algorithm for deciding symbolic equivalence between sets of constraint systems is implemented and performs well in practice. Unfortunately, it does not scale up well for deciding trace equivalence between processes. This is however the first implemented algorithm deciding trace equivalence on such a large class of processes.

Item Type: Article
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
Faculties > Sciences > School of Computing > Security Group
Depositing User: Vincent Cheval
Date Deposited: 23 Jan 2015 12:12 UTC
Last Modified: 02 Oct 2017 13:58 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/46882 (The current URI for this page, for reference purposes)
  • Depositors only (login required):

Downloads

Downloads per month over past year