A typing result for trace inclusion (for pair and symmetric encryption only)

Un résultat de typage pour l'inclusion de trace (pour le chiffrement symétrique et la paire).

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

1 CNRS - Centre National de la Recherche Scientifique
2 LSV - Laboratoire Spécification et Vérification [Cachan]
3 CNRS-L - National Council for Scientific Research = Conseil national de la recherche scientifique du Liban [Lebanon]
4 IRISA-D1 - SYSTÈMES LARGE ÉCHELLE
5 EMSEC - EMbedded SEcurity and Cryptography

Privacy-type properties such as vote secrecy, anonymity, or untraceability are typically expressed using the notion of trace equivalence in a process algebra that models security protocols. In this paper, we propose some results to reduce the search space when we are looking for an attack regarding trace equivalence. Our work is strongly inspired from [10], which establishes that, if there is a witness of non trace equivalence, then there is one that is well-typed. Our main contribution is to establish a similar result for trace inclusion. Our motivation is twofolds: first, this small attack property is needed for proving soundness of the tool SatEquiv [13]. Second, we revisit the proof in order to simplify it. Specifically, we show two results. First, if there is a witness of non-inclusion then there is one that is well-typed. We establish this result by providing a decision procedure for trace inclusion similar to the one proposed in [10] for trace equivalence. We also show that we can reduce the search space when considering the notion of static inclusion. Acutally, if there is a witness of static non-inclusion there is one of a specific shape. Even if our setting slightly differs from the one considered in [10], our proofs essentially follow the same ideas than the existing proof for trace equivalence. Nevertheless, we hope that this proof will be easier to extend to other primitives such as asymmetric encryption or signatures.

Les propriétés qui garantissent la préservation de la vie privée, comme le secret du vote, l'anonymat ou la non-traçabilité s'expriment à travers une notion d'équivalence de trace dans une algèbre de processus qui modélise les protocoles de sécurité. Dans ce papier, nous proposons des résultats pour réduire l'espace de recherche des attaques contre une telle équivalence. Notre travail s'inspire de [10], qui établit qu'il existe une attaque typée dès lors qu'il existe une attaque. Nous établissons un résultat similaire pour l'inclusion de trace, afin de prouver la correction de l'outil SatEquiv et de simplifier la preuve. D'une part, nous démontrons que s'il y a un témoin de non-inclusion, il y a un témoin typé en donnant une procédure de décision pour l'inclusion de trace similaire à celle de [10] pour l'équivalence. D'autre part, nous réduisons l'espace de recherche pour l'équivalence statique en démontrant que s'il existe un témoin de non-inclusion statique, il en existe un sous une certaine forme. Même si notre modèle diffère légèrement de celui considéré dans [10], nos preuves utilisent les mêmes idées. Néanmoins nous espérons que cette preuve sera plus facile à étendre au chiffrement asymétrique.

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

Véronique Cortier, Antoine Dallon, Stéphanie Delaune. A typing result for trace inclusion (for pair and symmetric encryption only). 2017. ⟨hal-01615265⟩