Efficiently deciding equivalence for standard primitives and phases

Décision efficace de l'équivalence de protocoles pour les primitives classiques et les phases

Véronique Cortier (1) , Antoine Dallon (2, 3, 1) , Stéphanie Delaune (4, 5, 6)

1 PESTO - Proof techniques for security protocols
2 LSV - Laboratoire Spécification et Vérification [Cachan]
3 IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires
4 EMSEC - EMbedded SEcurity and Cryptography
5 IRISA-D1 - SYSTÈMES LARGE ÉCHELLE
6 CNRS - Centre National de la Recherche Scientifique

Privacy properties like anonymity or untraceability are now well identified, desirable goals of many security protocols. Such properties are typically stated as equivalence properties. However, automatically checking equivalence of protocols often yields efficiency issues. We propose an efficient algorithm, based on graph planning and SAT-solving. It can decide equivalence for a bounded number of sessions, for protocols with standard cryptographic primitives and phases (often necessary to specify privacy properties), provided protocols are well-typed, that is encrypted messages cannot be confused. The resulting implementation , SAT-Equiv, demonstrates a significant speed-up w.r.t. other existing tools that decide equivalence, covering typically more than 100 sessions. Combined with a previous result, SAT-Equiv can now be used to prove security, for some protocols, for an unbounded number of sessions.

Les propriétés d'anonymat ou d'intraçabilité sont maintenant bien identifiées en tant que biens souhaitables de beaucoup de protocoles de sécurité. De telles propriétés s'expriment souvent à travers l'équivalence. Cependant, vérifier automatiquement l'équivalence de protocoles pose généralement des problèmes d'efficacité. Nous proposons un algorithme efficace, qui s'appuie sur la planification par résolution de formules SAT. Sur des protocoles contenant des primitives classiques et la phase, souvent nécessaire pour spécifier les propriétés d'équivalence, cet algorithme peut décider l'équivalence pour un nombre borné de sessions, à condition que les protocoles soient bien typés, c'est-à-dire que les messages ne puissent pas être confondus. L'implémentation de cet algorithme, SAT-Equiv, démontre une efficacité supérieure aux autres outils pour l'équivalence, et permet de couvrir jusqu'à 100 sessions. Avec l'aide d'un résultat précédent, SAT-Equiv peut maintenant être utilisé pour démontrer la sécurité pour un nombre non-borné de sessions, dans certains cas.

Domaines: Cryptographie et sécurité [cs.CR]

Véronique Cortier, Antoine Dallon, Stéphanie Delaune. Efficiently deciding equivalence for standard primitives and phases. 2018. ⟨hal-01819366⟩