Happy new year 2014!

A new publication related to the development of APTE was added: APTE: an Algorithm for Proving Trace Equivalence. This is a tool demonstration paper that will be published and presented in the Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’14).

Abstract: 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.

A new publication related to the development of APTE was added: Lengths may break privacy — or how to check for equivalences with length. This is a work done by Vincent Cheval, Véronique Cortier and Antoine Plet. It will be published in Proceedings of the 25th International Conference on Computer Aided Verification (CAV’13).

Abtract: Security protocols have been successfully analyzed using symbolic models, where messages are represented by terms and protocols by processes. Privacy properties like anonymity or untraceability are typically expressed as equivalence between processes. While some decision procedures have been proposed for automatically deciding process equivalence, all existing approaches abstract away the information an attacker may get when observing the length of messages.

In this paper, we study process equivalence with length tests. We first show that, in the static case, almost all existing decidability results (for static equivalence) can be extended to cope with length tests.
In the active case, we prove decidability of trace equivalence with length tests, for a bounded number of sessions and for standard primitives. Our result relies on a previous decidability result from Cheval et al (without length tests). Our procedure has been implemented and we have discovered a new flaw against privacy in the biometric passport protocol.

Current state of the implementation: The algorithm corresponding to the Theorem 2 was implemented in APTE v0.2alpha and sooner. It corresponds to the command “equivalence length” (see Tutorial). The algorithm corresponding to the Theorem 3 is yet to be implemented.