Protection de la vie privée : vers une analyse formelle et automatisée

Ces protocoles explicitent comment les différents agents communicants doivent se comporter et exploitent des primitives cryptographiques (e.g. chiffrement, signature) pour protéger les échanges.
Etant donné leur prédominance et leur importance, il est crucial de s’assurer que ces protocoles accomplissent réellement leurs objectifs. Parmi ces objectifs, on trouve de plus en plus de propriétés en lien avec la vie privée (eg. anonymat, non-traçabilité).

Malheureusement, les protocoles développés et déployés souffrent souvent de défauts de conception entraînant un cycle interminable entre découverte d'attaques et amélioration des protocoles.

Pour en sortir, nous prônons l'analyse mécanisée de ces protocoles par des méthodes formelles qui, via leurs fondements mathématiques, permettent une analyse rigoureuse apportant des garanties fortes sur la sécurité attendue. Parmi celles-ci, de grandes opportunités d'automatisation sont apportées par la vérification dans le modèle 'symbolique', où l'on peut déployer des techniques inspirées notamment de la logique et de la réécriture. La plupart des propriétés en lien avec la vie privée sont alors modélisées par l'équivalence entre deux systèmes.

Analyse des protocoles cryptographiques

Toutefois, vérifier cette équivalence est indécidable dans le cas général. Deux approches ont été proposées pour contourner ce problème.

Premièrement, pour un nombre borné de sessions d'un protocole, il est possible de symboliquement explorer toutes ses exécutions possibles et d'en déduire des procédures de décision pour l'équivalence.

Deuxièmement, il existe des méthodes de semi-décision du problème dans le cas général qui exploitent des abstractions, notamment en considérant une forme forte d'équivalence.

Nous avons identifié un problème majeur pour chacune des deux méthodes de l'état de l'art qui limitent grandement leur impact en pratique.

Premièrement, les méthodes et outils qui explorent symboliquement les exécutions souffrent de l'explosion combinatoire du nombre d'états, causée par la nature concurrente des systèmes étudiés.

Deuxièmement, dans le cas non borné, la forme forte d'équivalence considérée se trouve être trop imprécise pour vérifier certaines propriétés telle que la non traçabilité, rendant cette approche inopérante pour ces propriétés.

Vers de meilleures techniques de sécurité

Dans cette thèse, nous proposons une solution à chacun des problèmes. Ces solutions prennent la forme de contributions théoriques, mais nous nous efforçons de les mettre en pratique via des implémentations afin de confirmer leurs impacts pratiques qui se révèlent importants.

Tout d'abord, nous développons des méthodes de réduction d'ordres partiels pour réduire drastiquement le nombre d'états à explorer tout en s'assurant que l'on ne perd pas d'attaques.

Nos méthodes sont conçues pour le cadre exigeant de la sécurité et sont prouvées correctes et complètes vis-à-vis de l'équivalence. Nous montrons comment elles peuvent s'intégrer naturellement dans les outils existants. Nous prouvons la correction de cette intégration dans un outil et proposons une implémentation complète. Finalement, nous mesurons le gain significatif en efficacité ainsi obtenu et nous en déduisons que nos méthodes permettent l'analyse d'un plus grand nombre de protocoles.

Ensuite, pour résoudre le problème de précision dans le cas non-borné, nous proposons une nouvelle démarche via la mise en place de conditions suffisantes permettant de garantir le respect de la vie privée.
Nous définissons deux propriétés qui impliquent systématiquement la non-traçabilité et l'anonymat et qui sont facilement vérifiables via les outils existants (e.g. ProVerif).

Nous avons implémenté un nouvel outil qui met en pratique cette méthode résolvant le problème de précision de l'état de l'art pour une large classe de protocoles. Cette nouvelle approche a permis les premières analyses de plusieurs protocoles industriels incluant des protocoles largement déployés, ainsi que la découverte de nouvelles attaques.