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.