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.

GitHub repository and new contributor

A GitHub repository has been created : 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 !

The mailing list is now available

A mailing list for general discussions on APTE is now available. I will use the mailing list to announce any new release of APTE or update of the website. Moreover, feel free to use this mailing list to post your remarks, questions or even bug reports.

A webpage is also available (see the menu or click here) regrouping the instructions on how to subscribe / post / unsubscribe. This webpage will also contain the archive of the mailing list.