A new publication : Lengths may break privacy — or how to check for equivalences with length

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.



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.


Publications webpage

A webpage containing all the publications related to APTE, Algorithm for Proving Trace Equivalence is now available.

Eventually, this webpage will also list the different usages of APTE in the academic literature of computer science. As such, do not hesitate to send an email at v.f.p.cheval@cs.bham.ac.uk if you want your paper/tool/… to be listed on this webpage.

Minor release: APTE v0.3.1beta

A minor release of APTE soon after the major release of v0.3beta. You can download it here or on the download page.

New features:

  • Fix of a stack overflow problem.
  • The parser now handles properly the declared constants
  • Addition of three new examples: Unlinkability of the Passive Authentication protocol of the electronic passport (without considering length, the existing attack when considering the length of messages and lastly the fix)

Since APTE is still in a beta version, there will probably be regular releases until the release of the first stable version. Do not hesitate to send examples of processes or bug reports at cheval@lsv.ens-cachan.fr or v.f.p.cheval@cs.bham.ac.uk.