Formal Verification for Real-World Cryptographic Protocols and Implementations

Abstract : Individuals and organizations are increasingly relying on the Web and on user-facing applications for use cases such as online banking, secure messaging, document sharing and electronic voting. To protect the confidentiality and integrity of these communications, these systems depend on authentication and authorization protocols, on application-level cryptographic constructions and on transport-layer cryptographic protocols. However, combining these varied mechanisms to achieve high-level security goals is error-prone and has led to many attacks even on sophisticated and well-studied applications. This thesis aims to develop methods and techniques for reasoning about, designing and implementing cryptographic protocols and secure application components relevant to some of the most frequently used cryptographic protocols and applications. We investigate and formalize various notions of expected guarantees and evaluate whether some of the most popular secure channel protocols, such as secure messaging protocols and transport protocols often operating at the billion-user scale, are capable of meeting these goals. In this thesis, we ask: can existing major paradigms for formal protocol verification serve as guidelines for the assessment of existing protocols, the prototyping of protocols being designed, and the conception of entirely new protocols, in a way that is meaningful and reflective of their expected real-world properties? And can we develop novel frameworks for formal verification and more secure implementation based on these foundations? We propose new formal models in both symbolic and computational formal verification frameworks for these protocols and applications. In some of the presented work, we obtain a verification methodology that starts from the protocol and ends at the implementation code. In other parts of our work, we develop a dynamic framework for generating formal verification models for any secure channel protocol described in a lightweight syntax. Ultimately, this thesis presents formal verification approaches for existing protocols reaching towards their implementation as well as methods for prototyping and formally verifying new protocols as they are being drafted and designed.
Complete list of metadatas

Cited literature [100 references]  Display  Hide  Download

https://hal.inria.fr/tel-01950884
Contributor : Nadim Kobeissi <>
Submitted on : Saturday, February 2, 2019 - 5:16:22 PM
Last modification on : Wednesday, February 6, 2019 - 9:09:25 AM
Long-term archiving on : Friday, May 3, 2019 - 4:34:02 PM

File

thesis.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : tel-01950884, version 2

Collections

Citation

Nadim Kobeissi. Formal Verification for Real-World Cryptographic Protocols and Implementations. Computer Science [cs]. INRIA Paris; Ecole Normale Supérieure de Paris - ENS Paris, 2018. English. ⟨tel-01950884v2⟩

Share

Metrics

Record views

471

Files downloads

275