Kobeissi, Nadim
[Author]
;
Paris Sciences et Lettres (ComUE)
[Contributor];
Bhargavan, Karthikeyan
[Contributor];
Blanchet, Bruno
[Contributor]
Formal verification for real-world cryptographic protocols and implementations ; Vérification formelle des protocoles et des implementations cryptographiques
You can manage bookmarks using lists, please log in to your user account for this.
Media type:
Text;
Electronic Thesis;
E-Book
Title:
Formal verification for real-world cryptographic protocols and implementations ; Vérification formelle des protocoles et des implementations cryptographiques
Footnote:
Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
Description:
Les particuliers et les organisations comptent de plus en plus sur le Web et sur les applications destinées aux utilisateurs pour des cas d'utilisation comme les services bancaires en ligne, la messagerie sécurisée, le partage de documents et le vote électronique. Pour protéger la confidentialité et l'intégrité de ces communications, ces systèmes dépendent de protocoles d'authentification et d'autorisation, de constructions cryptographiques au niveau de l'application et de protocoles cryptographiques au niveau du transport. Cependant, la combinaison de ces divers mécanismes pour atteindre des objectifs de sécurité de haut niveau est sujette à l'erreur et a conduit à de nombreuses attaques, même contre des applications sophistiquées et bien étudiées. Cette thèse vise à développer des méthodes et des techniques de raisonnement, de conception et de mise en œuvre de protocoles cryptographiques et de composants d'application sécurisés pertinents pour certains des protocoles et applications cryptographiques les plus fréquemment utilisés. Nous étudions et formalisons diverses notions de garanties attendues et évaluons si certains des protocoles de canaux sécurisés les plus populaires, tels que les protocoles de messagerie sécurisée et les protocoles de transport fonctionnant souvent à l'échelle du milliard d'utilisateurs, sont capables d'atteindre ces objectifs. Dans cette thèse, nous posons la question suivante : les principaux paradigmes existants pour la vérification formelle des protocoles peuvent-ils servir de lignes directrices pour l'évaluation des protocoles existants, le prototypage des protocoles en cours de conception et la conception de protocoles entièrement nouveaux, d'une manière qui soit significative et qui reflète leurs propriétés réelles prévues ? Et pouvons-nous développer de nouveaux cadres pour une vérification formelle et une mise en œuvre plus sûre sur la base de ces fondements ? Nous proposons de nouveaux modèles formels dans des cadres de vérification formelle à la fois symboliques et ...