Welcome to the new website for the automatic cryptographic protocol verifier APTE: Algorithm for Proving Trace Equivalence. This tool is a decision procedure for proving trace equivalence between two processes for a bounded number of sessions. Trace equivalence can be used to model cryptographic security properties such that privacy, anonymity, unlinkability, receipt-freeness… APTE can handle several cryptographic primitives: symmetric and asymmetric encryption / decryption, digital signature, hash functions, pairing and any one-way function.

All the new versions of APTE will be available for download on this website.

Feel free to leave comments or questions on the mailing list.

ETAPS 2014

This year’s edition of ETAPS was a good one for APTE. During the security conference of ETAPS, namely Conference on Principles of Security and Trust (POST), two papers mentioned and worked on APTE: The first paper is by D. Baelde, S. Delaune and L. Hirschi, is entitled A reduced semantics for deciding trace equivalence using constraint systems, and directly contributes to the development of APTE thanks Lucca Hirschi. The second paper is by M. Backes, E. Mohammadi and T. Ruffing, and is entitled Computational Soundness Results for ProVerif.

A reduced semantics for deciding trace equivalence using constraint systems

Abstract: Many privacy-type properties of security protocols can be modelled using trace equivalence properties in suitable process algebras. It has been shown that such properties can be decided for interesting classes of finite processes (i.e., without replication) by means of symbolic execution and constraint solving. However, this does not suffice to obtain practical tools. Current prototypes suffer from a classical combinatorial explosion problem caused by the exploration of many interleavings in the behaviour of processes. Modersheim et al. have tackled this problem for reachability properties using partial order reduction techniques. We revisit their work, generalize it and adapt it for equivalence checking. We obtain an optimization in the form of a reduced symbolic semantics that eliminates redundant interleavings on the fly.

Computational Soundness Results for ProVerif

Dolev-Yao models of cryptographic operations constitute the foundation of many successful verification tools for security protocols, such as the protocol verifier ProVerif. Research over the past decade has shown that many of these symbolic abstractions are computationally sound, i.e., the absence of attacks against the abstraction entails the security of suitable cryptographic realizations. Most of these computational soundness (CS) results, however, are restricted to trace properties such as authentication, and the few promising results that strive for CS for the more comprehensive class of equivalence properties, such as strong secrecy or anonymity, either only consider a limited class of protocols or are not amenable to fully automated verification.

In this work, we identify a general condition under which CS for trace properties implies CS for uniformity of bi-processes, i.e., the class of equivalence properties that ProVerif is able to verify for the applied pi-calculus. As a case study, we show that this general condition holds for a Dolev-Yao model that contains signatures, public-key encryption, and corresponding length functions. We prove this result in the CoSP framework (a general framework for establishing CS results). To this end, we extend the CoSP framework to equivalence properties, and we show an existing embedding of the applied pi-calculus to CoSP can be re-used for uniform bi-processes. On the verification side, as analyses in ProVerif with symbolic length functions often do not terminate, we show how to combine the recent protocol verifier APTE with ProVerif. As a result, we establish a computationally sound automated verification chain for uniformity of bi-processes in the applied pi-calculus that use public-key encryption, signatures, and length functions.

Happy new year! 2014 starts well with a new publication!

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.

Release v0.4beta : Time for some statistics !

A new version of APTE have been released : APTE v0.4beta. As previously mentioned, it can be both downloaded through the download webpage or directly through the GitHub release webpage.

This release is mainly focused on the API of APTE, by fixing some bugs and also providing a new set of statistics on the algorithm’s executions. Moreover, it allows a user to select different strategies to be used in the execution of the algorithm.

New features:

  • Correction of a bug in the parser with the tuples.
  • Addition of a module for statistic on the matrices generated by the algorithm
  • New strategies for the algorithm available (see the different new options)
  • An log option have been added that stores the tree of matrices. It should help following the generation of matrices by the algorithm.
  • The help menu have been changed to match all the new options
  • Addition of new examples.

GitHub repository and new contributor

A GitHub repository has been created : https://github.com/APTE/APTE/. All the development versions of APTE will be available there as well as the different releases. Nevertheless, it will still be possible to download the stable versions of APTE directly from the Download page of this website.

A new contributor joined the project : Lucca Hirschi. He is a PhD student in the Laboratoire Spécification et Vérification and he is implementing a new feature that aims to improve the performance of the tool.

Minor release: APTE v0.3.2beta

A minor release to fix some compilation issues on Linux. You can download it here or on the download page.

New features:

  • Fixing an issue with the Makefile which went into an infinite loop on Linux.
  • Cleaning of the archive of some MACOX files

Thank you for the bug report !