SAT-Equiv

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).

La version longue est également disponible ici.

Sources

Installation

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 :

Résultats expérimentaux

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

À 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 AkissDeepsec 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