APTE: An Algorithm for Proving Trace Equivalence

Cheval, Vincent (2014) APTE: An Algorithm for Proving Trace Equivalence. In: Ábrahám, Erika and Havelund, Klaus, eds. Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, 8413. Springer-Verlag Berlin, Grenoble, France pp. 587-592. ISBN 978-3-642-54861-1. E-ISBN 978-3-642-54862-8. (doi:https://doi.org/10.1007/978-3-642-54862-8_50) (Full text available)


This paper presents APTE, a new tool for automatically proving the security of cryptographic protocols. It focuses on proving trace equivalence between processes, which is crucial for specifying privacy type properties such as anonymity and unlinkability. The tool can handle protocols expressed in a calculus similar to the applied-pi calculus, which allows us to capture most existing protocols that rely on classical cryptographic primitives. In particular, APTE handles private channels and else branches in protocols with bounded number of sessions. Unlike most equivalence verifier tools, APTE is guaranteed to terminate Moreover, APTE is the only tool that extends the usual notion of trace equivalence by considering ``side-channel'' information leaked to the attacker such as the length of messages and the execution times. We illustrate APTE on different case studies which allowed us to automatically (re)-discover attacks on protocols such as the Private Authentication protocol or the protocols of the electronic passports.

Item Type: Conference or workshop item (Paper)
Uncontrolled keywords: Cryptographic protocols, Formal verification, Symbolic model, Automatic, Equivalence properties, Timing attacks, Lengh attacks, 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:35 UTC
Last Modified: 23 Jan 2015 11:35 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/46724 (The current URI for this page, for reference purposes)
  • Depositors only (login required):


Downloads per month over past year