Vérification automatique de la protection de la vie privée : entre théorie et pratique

The information society we belong to heavily relies on secure information exchanges. To exchange information securely, one should use security protocols that specify how communicating agents should behave notably by using cryptographic primitives (e.g. encryption, signature). Given their ubiquitous and critical nature, we need to reach an extremely high level of confidence that they actually meet their goals. Those goals can be various and depend on the usage context but, more and more often, they include privacy properties (e.g. anonymity, unlinkability). Unfortunately, designed and deployed security protocols are often flawed and critical attacks are regularly disclosed, even on protocols of utmost importance, leading to the never-ending cycle between attack and fix.To break the present stalemate, we advocate the use of formal methods providing rigorous, mathematical frameworks and techniques to analyse security protocols. One such method allowing for a very high level of automation consists in analysing security protocols in the symbolic model and modelling privacy properties as equivalences between two systems. Unfortunately, deciding such equivalences is actually undecidable in the general case. To circumvent undecidability, two main approaches have emerged. First, for a bounded number of agents and sessions of the security protocol to analyse, it is possible to symbolically explore all possible executions yielding decision procedures for equivalence between systems. Second, for the general case, one can semi-decide the problem leveraging dedicated abstractions, notably relying on a strong form of equivalence (i.e. diff-equivalence).The two approaches, i.e. decision for the bounded case or semi-decision for the unbounded case, suffer from two different problems that significantly limit their practical impact. First, (symbolically) exploring all possible executions leads to the so-called states space explosion problem caused by the concurrency nature of security protocols. Concerning the unbounded case, diff-equivalence is actually too imprecise to meaningfully analyse some privacy properties such as unlinkability, nullifying methods and tools relying on it for such cases.In the present thesis, we address those two problems, going back and forth between theory and practice. Practical aspects motivate our work but our solutions actually take the form of theoretical developments. Moreover, we make the effort to confirm practical relevance of our solutions by putting them into practice (implementations) on real-world case studies (analysis of real-world security protocols).First, we have developed new partial order reduction techniques in order to dramatically reduce the number of states to explore without loosing any attack. We design them to be compatible with equivalence verification and such that they can be nicely integrated in frameworks on which existing procedures and tools are based. We formally prove the soundness of such an integration in a tool and provide a full implementation. We are thus able to provide benchmarks showing dramatic speedups brought by our techniques and conclude that more protocols can henceforth be analysed.Second, to solve the precision issue for the unbounded case, we propose a new methodology based on the idea to ensure privacy via sufficient conditions. We present two conditions that always imply unlinkability and anonymity that can be verified using existing tools (e.g. ProVerif). We implement a tool that puts this methodology into practice, hence solving the precision issue for a large class of protocols. This novel approach allows us to conduct the first formal analysis of some real-world protocols (some of them being widely deployed) and the discovery of novel attacks.La société de l’information dans laquelle nous vivons repose notamment sur notre capacité à échanger des informations de façon sécurisée. Ces échanges sécurisés sont réalisés au moyen de protocoles cryptographiques. Ils explicitent comment les différents agents communicants doivent se comporter et exploitent des primitives cryptographiques (e.g. chiffrement, signature) pour protéger les échanges. Étant 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 (e.g. 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, la vérification dans le modèle symbolique offre de grandes opportunités d’automatisation. 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. Toutefois, vérifier cette équivalence est indécidable dans le cas général. Deux approches ont alors émergé. 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èmenent, 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.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 qui consiste à assurer la vie privée via des conditions suffisantes. 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