Université de Rennes 1 Vérification formelle de la non-traçabilité pour les protocoles à état : entre modèles symboliques et calculatoires Formal verification of unlinkability for stateful protocols : bridging the gap between symbolic and computational models méthodes formellessécurité informatiqueprotocoles cryptographiquesnon-traçabilité formal methodssecurity cryptographic protocolsunlinkabilitystateful Méthodes formelles (informatique) Cryptographie Systèmes informatiques -- Mesures de sûreté La dépendance de plus en plus grande à l'égard des systèmes informatiques soulève d'importantes questions en terme de vie privée, et nécessite notamment des protocoles de communication garantissant des propriétés de sécurité telles que la non-traçabilité. Spécifier formellement cette propriété est difficile et dépendant du contexte, et la vérifier est d'autant plus complexe. Fournir des bases mathématiques solides et des méthodes assistées par ordinateur devient donc crucial, mais les techniques actuelles ne sont pas satisfaisantes pour analyser la non-traçabilité des protocoles à état. Dans ce manuscrit de thèse, nous abordons à la fois la question de la modélisation et de la vérification. Tout d'abord, nous proposons une définition précise de non-traçabilité et expliquons pourquoi les notions actuelles ne sont pas adaptées à notre classe de protocoles à état. Ensuite, nous abordons la question de la vérification assistée par ordinateur. Nous développons deux approches, illustrées par des études de cas. Notre première approche est une méthode de vérification basée sur des conditions suffisantes dans le modèle symbolique. Notre deuxième approche est un cadre théorique et un assistant de preuve interactif permettant de mécaniser des preuves de protocoles cryptographiques pour un nombre arbitraire de sessions dans le modèle calculatoire. The ever-increasing dependency on computer systems justifies significant concerns over privacy, and notably calls for communication protocols that ensure some security properties such as unlinkability. Formally specifying this property is difficult and context-dependent, and verifying it is complex. Therefore, providing solid mathematical foundations and computer-assisted methods is becoming crucial, but current techniques are not sufficient to analyze unlinkability for stateful protocols. In this manuscript, we address both the modelling issue and the verification issue. We first propose a precise definition of unlinkability and discuss how existing notions are inadequate for our class of stateful protocols. Then, we address the issue of computer-assisted verification. We develop two approaches, both illustrated with case studies. Our first approach is a verification method based on sufficient conditions in the symbolic model. Our second approach is a framework and an interactive prover allowing us to mechanize proofs of security protocols for an arbitrary number of sessions in the computational model. Electronic Thesis or DissertationText en application/pdf1 : 1711 Kohttps://ged.univ-rennes1.fr/nuxeo/site/esupversions/ad51b228-c67a-4f41-a894-4fa14795b58a Moreau Solène 1993-11-22 FR 259945455 solene.moreau@posteo.org 2021REN1S068 http://www.theses.fr/2021REN1S068 2021-11-18 Informatique Universite de Rennes 1thesis.degree.grantor_1 02778715X Doctorat non ouiDelauneStéphanieintervenant_1109561384BaeldeDavidintervenant_2201647249PinchinatSophieintervenant_3097578754BanaGergeiintervenant_6259945587KremerSteveintervenant_4153809027TiuAlwenintervenant_5237637839 MATHSTICecoleDoctorale_1 204770424 IRISA partenaireRecherche_1 026386909 ddc:004 DelauneStéphanieBaeldeDavidPinchinatSophieKremerSteveTiuAlwenBanaGergeiUniversite de Rennes 1Sciences et technologie, medecine, pharmacie, odontologie, droit, economie, gestion, philosophieMATHSTICÉcole doctorale Mathématiques et sciences et technologies de l'information et de la communication (Rennes) IRISA ASCII PDF 1752109