Formalizing and proving a typing result for security protocols in Isabelle/HOL

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review


There are several works on the formalization of security protocols and proofs of their security in Isabelle/HOL; there have also been tools for automatically generating such proofs. This is attractive since a proof in Isabelle gives a higher assurance of the correctness than a pen-and-paper proof or the positive output of a verification tool. However several of these works have used a typed model, where the intruder is restricted to "well-typed" attacks. There also have been several works that show that this is actually not a restriction for a large class of protocols, but all these results so far are again pen-and-paper proofs. In this work we present a formalization of such a typing result in Isabelle/HOL. We formalize a constraint-based approach that is used in the proof argument of such typing results, and prove its soundness, completeness and termination. We then formalize and prove the typing result itself in Isabelle. Finally, to illustrate the real-world feasibility, we prove that the standard Transport Layer Security (TLS) handshake satisfies the main condition of the typing result.
Original languageEnglish
Title of host publicationProceedings of 2017 IEEE 30th Computer Security Foundations Symposium
Publication date2017
ISBN (Print)9781538632161
Publication statusPublished - 2017
Event2017 IEEE 30th Computer Security Foundations Symposium - Santa Barbara, United States
Duration: 21 Aug 201725 Sep 2017


Conference2017 IEEE 30th Computer Security Foundations Symposium
Country/TerritoryUnited States
CitySanta Barbara
SeriesI E E E Computer Security Foundations Symposium. Proceedings


Dive into the research topics of 'Formalizing and proving a typing result for security protocols in Isabelle/HOL'. Together they form a unique fingerprint.

Cite this