Several examples files are provided in the source code archive of APTE, most of them coming from academic papers, others for testing purposes only. On this webpage will be listed interesting protocols with their security properties that APTE can take as input. We will also put on this webpage protocol that APTE is suppose to handle but take too much time to obtain a result. They will be part of the benchmark for futur releases of APTE.

The private authentication protocol

• The original protocol: one session, two sessions and three sessions.
• The possible fixes to deal with timing attack: PA-fix1, PA-fix2 and PA-fix3. The files include the transformation to decide time trace equivalence. They only focus on one session of the protocol.

We have compiled some statistics on the execution of the tool on the private authentication protocol. More specifically, we looked at the execution of the symbolic equivalence on all unfolded symbolic traces. Hence the statistics here do not correspond to the fastest strategy but the naive strategy depicted in [Che12].

Each line of this table corresponds to some statistic about symbolic traces of the given size. The column “Nb traces” corresponds to the number of traces, the column “Nb rules” corresponds to the number of rules (see [Che12]) that was applied to decide all symbolic equivalences for traces of this size. The columns % internal and % external indicate the percentage of internal and external rules.
Lastly, the number of columns corresponds to the number of columns in the matrices of constraint systems handled by the tool when deciding the symbolic equivalence.

This table of statistic was compiled with the statistics provided by the following command line.

./apte -no_comm -unfold -display size -verbose Example/Private_Authentication_Protocol.txt 

This table of statistic was compiled with the statistics provided by the following command line.

./apte -no_comm -unfold -display size -verbose Example/Private_Authentication_Protocol_2_sessions.txt 

At some point, the algorithm takes too much time to process so the statistics does not above traces of size 9. For three sessions of the protocol, we only computed the size of the matrices generated after unfolding.

This table of statistic was compiled with the statistics provided by the following command line.

./apte -no_comm -unfold 0 -display size -verbose Example/Private_Authentication_Protocol_3_sessions.txt