Typing messages for free in security protocols

Un résultat de typage pour les protocoles de sécurité

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

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

Security properties of cryptographic protocols are typically expressed as reachability or equivalence properties. Secrecy and authentication are examples of reachability properties while privacy properties such as untraceability, vote secrecy, or anonymity are generally expressed as behavioural equivalence in a process algebra that models security protocols. Our main contribution is to reduce the search space for attacks for reachability as well as equivalence properties. Specically, we show that if there is an attack then there is one that is well-typed. Our result holds for a large class of typing systems, a family of equational theories that encompasses all standard primitives, and a large class of deterministic security protocols. For many standard protocols, we deduce that it is sufficient to look for attacks that follow the format of the messages expected in an honest execution, therefore considerably reducing the search space.

Les propriétés de sécurité des protocoles cryptographiques sont habituellement formalisés comme des propriétés d'accessibilité ou d'équivalence. Le secret et l'authentification s'expriment comme des propriétés d'accessibilité, tandis que l'intraçabilité, le secret du vote ou l'anonymat sont modélisés par une équivalence dans une algèbre de processus. Comme contribution principale, nous réduisons l'espace de recherche pour les attaques contre l'accessibilité et l'équivalence. Plus précisément, nous montrons que s'il existe une attaque alors il en existe une bien typée. Ce résultat vaut pour une large classe de systèmes de typages, une famille de théories équationnelles qui autorise toutes les primitives usuelles, et une classe importante de protocoles de sécurité déterministes. Pour la plupart des protocoles usuelle, il suffit donc de considérer des attaques qui suivent le format des messages attendus dans une exécution honnête, ce qui réduit considérable l'espace de recherche.

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

Rémy Chrétien, Véronique Cortier, Antoine Dallon, Stéphanie Delaune. Typing messages for free in security protocols. [Research Report] LSV, ENS Cachan, CNRS, INRIA, Université Paris-Saclay, Cachan (France). 2018, pp.1-49. ⟨hal-01741172⟩