SAT-Equiv

SAT-Equiv est un outil libre pour la vérification d'équivalences de protocoles cryptographiques. Il procède par réduction vers les problèmes de planification et les formules SAT. La dernière version est suffisamment efficace pour traiter des centaines de sessions et parfois atteindre la vérification d'un nombre arbitraire de sessions.

Cet outil a été décrit dans les publications suivantes (voir ci-dessous pour les fichiers d'exemple et les sources).

Véronique Cortier, Antoine Dallon, and Stéphanie Delaune. Efficiently deciding equivalence for standard primitives and phases, à paraître à ESORICS'18 (PDF, PDF (version longue)).
Véronique Cortier, Antoine Dallon, and Stéphanie Delaune. SAT-Equiv: an efficient tool for equivalence properties, in Proceedings of the 30th IEEE Computer Security Foundations Symposium (CSF'17), Santa Barbara, California, USA, August 2017, pages 481-494. IEEE Computer Society Press. (PDF, PDF (version longue), BibTeX + Résumé).

La version longue est également disponible ici.

Sources

SAT-Equiv 0.1 (version de CSF'17)
SAT-Equiv 0.2
SAT-Equiv 0.3 (version d'ESORICS'18).

Installation

SAT-Equiv réalise une réduction vers une formule SAT, qu'elle donne ensuite à un solveur SAT. Il faut donc commencer par installer minisat. Sous Debian/Ubuntu, il suffit d'utiliser apt-get install minisat.
Désarchiver les sources par la commande tar -zxvf satequiv-0.3.tar.gz
Dans le dossier SAT-Equiv, exécuter make. Une version récente d'OCaml est nécessaire (la version 4.04.2 fonctionne).
Le programme satequiv est apparu.
Il est possible de tester ./satequiv Examples/Denning-Sacco-B/ds-3.pi qui doit donner une réponse rapide.
La liste des options est disponible par ./satequiv --help.
Plus d'informations se trouvent dans le README.

Pour toute question, n'hésitez pas à me contacter à l'adresse name@lsv.fr en remplaçant nom par dallon.

Licence

SAT-Equiv est distribué sous la licence GNU AGPL.

Comparaisons

Autres outils

Les outils référencés, dont j'indique la version utilisée dans l'article présenté à ESORICS'18 et dans ma thèse, sont les suivants :

SPEC (Version 0.3, telle qu'au 18 janvier 2017) ;
Akiss (tel qu'au 24 octobre 2017) ;
Deepsec (tel qu'au le 22 avril 2018) ;
SAT-Equiv 0.1 et 0.3.

Résultats expérimentaux

Les raisons pour lesquelles les comparaisons ont été arrêtées sont au nombre de trois :

Dépassement de la limite de temps (TO) après plus de 24h ;
Dépassement de la limite de mémoire (MO) lorsque l'outil utilise plus de 128Go de RAM ;
Dépassement de la taille de la pile (SO) quand une exception Stack Overflow a été levée.

À titre d'exemple, nous donnons deux tables de résultats. D'autres sont disponibles dans la version longue (voir ci-dessus).

Un exemple symétrique : le protocole de Yahalom-Paulson

	SPEC	Akiss	Deepsec	v. 0.1 (CSF'17)	v. 0.3 (ESORICS'18)
3	23m	7s	10ms	50s	400ms
6	MO	TO	900ms	165m	5s
7			6s	TO	17s
10			85m		63s
12			TO		143s
14					6m
21					155m
28					7h

Un exemple assymétrique : le protocole Active Authentication

	SPEC	Akiss	Deepsec	SAT-Equiv
4	15m	3s	0s	0.01s
6	MO	5m	0.02s	0.07s
8		SO	0.02s	0.07s
46			23h50m	0.9s
50			TO	1.1s
80				3s
200				18s
400				78s

Fichiers d'exemples

Les fichiers d'exemples pour ma thèse de doctorat se trouvent ici.
Les fichiers d'exemple pour ESORICS'18 se trouvent ici. Les fichiers d'exemples de SAT-Equiv sont également fournis avec l'outil.
Les fichiers de la comparaison parue à CSF'17 pour les outils SAT-Equiv, APTE, AKISS et SPEC se trouvent derrière ce lien.