Representative Publications
[R1] Formal verification of standards for distance vector routing protocols (Karthikeyan Bhargavan, Davor Obradovic, Carl A. Gunter), In Journal of the ACM (JACM), volume 49, 2002. [bib] [pdf]
[R2] A Messy State of the Union: Taming the Composite State Machines of TLS (Benjamin Beurdouche, Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub, Jean Karim Zinzindohoue), In IEEE Symposium on Security & Privacy (Oakland), 2015. (Distinguished Paper Award) [bib] [pdf]
[R3] Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate (Karthikeyan Bhargavan, Bruno Blanchet, Nadim Kobeissi), In IEEE Symposium on Security and Privacy (Oakland), 2017. (Distinguished Paper Award) [bib] [pdf]
2019
[78] A Mechanised Cryptographic Proof of the WireGuard Virtual Private Network Protocol (, and ), In IEEE European Symposium on Security and Privacy (EuroS&P), . [bibtex] [url]
[77] Formally Verified Cryptographic Web Applications in WebAssembly (, , and ), In IEEE Symposium on Security and Privacy (S&P), . [bibtex] [url]
[76] Noise Explorer: Fully Automated Modeling and Verification for Arbitrary Noise Protocols (, and ), In IEEE European Symposium on Security and Privacy (EuroS&P), . [bibtex] [url]
[75] Imperfect forward secrecy: how Diffie-Hellman fails in practice (, , , , , , , , , , , , and ), In Commun. ACM, volume 62, . [bibtex] [url]
2018
[74] hacspec: towards verifiable cryptographic standards (, and ), In Security Standardization Research (SSR), . [bibtex] [pdf]
[73] A Formal Treatment of Accountable Proxying Over TLS (, , and ), In IEEE Symposium on Security and Privacy (Oakland), . [bibtex] [pdf]
2017
[72] Automated Verification for Secure Messaging Protocols and their Implementations: A Symbolic and Computational Approach (, and ), In IEEE European Symposium on Security and Privacy (EuroS&P), . [bibtex] [url]
[71] Content delivery over TLS: a cryptographic analysis of Keyless SSL (), In IEEE European Symposium on Security and Privacy (EuroS&P), . [bibtex] [url]
[70] Formal Modeling and Verification for Domain Validation and ACME ( and ), In Financial Cryptography and Data Security (FC), . [bibtex] [url]
[69] Verified low-level programming embedded in F* (, , , , , , , , , and ), In Proceedings of the ACM on Programming Languages (PACMPL), volume 1, . [bibtex] [pdf]
[68] Implementing and Proving the TLS 1.3 Record Layer (, , , , , , , and ), In IEEE Symposium on Security and Privacy (Oakland), . [bibtex] [pdf]
[67] Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate (, and ), In IEEE Symposium on Security and Privacy (Oakland), . [bibtex] [url]
[66] Everest: Towards a Verified, Drop-in Replacement of HTTPS (, , , , , , , , , , , , , , , , , , , and ), In Summit on Advances in Programming Languages (SNAPL), . [bibtex] [pdf]
[65] HACL*: A Verified Modern Cryptographic Library (, , and ), In Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, Dallas, TX, USA, October 30 - November 03, 2017, . [bibtex] [pdf]
[64]A Messy State of the Union: Taming the Composite State Machines of TLS (, , , , , , and ), In Communications of the ACM, volume 60, . [bibtex]
2016
[63] Dependent Types and Multi-Monadic Effects in F* (, , , , , , , , , , and ), In 43nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), . [bibtex] [pdf]
[62] Transcript Collision Attacks: Breaking Authentication in TLS, IKE, and SSH ( and ), In Proceedings of the ISOC Network and Distributed System Security Symposium (NDSS '16), . [bibtex] [pdf]
[61] A Verified Extensible Library of Elliptic Curves (, and ), In IEEE Computer Security Foundations Symposium (CSF), . [bibtex] [url]
[60]Formal Verification of Smart Contracts: Short Paper (, , , , , , , and ), In Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security (PLAS), . [bibtex]
[59] Downgrade Resilience in Key-Exchange Protocols (, , , , and ), In IEEE Symposium on Security & Privacy (Oakland), . [bibtex] [url]
[58] ProScript-TLS: Verifiable Models and Systematic Testing for TLS 1.3 ( and ), . [bibtex] [pdf]
[57]miTLS: Verifying Protocol Implementations against Real-World Attacks (, and ), In IEEE Security & Privacy Magazine, volume 14, . [bibtex]
[56] On the Practical (In-)Security of 64-bit Block Ciphers ( and ), In ACM Conference on Computer and Communications Security (CCS'16), . [bibtex] [pdf]
2015
[55] Verified Contributive Channel Bindings for Compound Authentication (, and ), In Network and Distributed System Security Symposium (NDSS '15), . [bibtex] [pdf]
[54] A Messy State of the Union: Taming the Composite State Machines of TLS (, , , , , , and ), In IEEE Symposium on Security & Privacy (Oakland), . [bibtex] [pdf]
[53] Network-based Origin Confusion Attacks against HTTPS Virtual Hosting ( and ), In International Conference on World Wide Web (WWW'15), . [bibtex] [pdf]
[52] Imperfect Forward Secrecy: How Diffie-Hellman Fails in Practice (, , , , , , , , , , , , , and ), In ACM Conference on Computer and Communications Security (CCS'15), . [bibtex] [pdf]
[51] FLEXTLS: A Tool for Testing TLS Implementations (, , , and ), In USENIX Workshop on Offensive Technologies (WOOT'15), . [bibtex] [pdf]
2014
[50] Discovering concrete attacks on website authorization by formal analysis (, , and ), In Journal of Computer Security, volume 22, . [bibtex] [pdf]
[49] Proving the TLS Handshake Secure (as it is) (, , , , and ), In CRYPTO, . [bibtex] [url]
[48] Gradual typing embedded securely in JavaScript (, , , , , and ), In The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '14), . [bibtex] [pdf]
[47] Defensive JavaScript - Building and Verifying Secure Web Components (, and ), Chapter in Foundations of Security Analysis and Design VII, FOSAD Tutorial Lectures, Springer Verlag, volume 8604, . [bibtex] [pdf]
[46] Triple Handshakes and Cookie Cutters: Breaking and Fixing Authentication over TLS (, , , and ), In IEEE Symposium on Security & Privacy (Oakland), . [bibtex] [pdf]
2013
[45] Keys to the Cloud: Formal Analysis and Concrete Attacks on Encrypted Web Storage (, , and ), In 2nd Conference on Principles of Security and Trust (POST 2013) (David Basin, John Mitchell, eds.), Springer Verlag, . [bibtex] [pdf]
[44] Towards Unified Authorization for Android ( and ), In 5th International Symposium on Engineering Secure Software and Systems (ESSoS 2013), . [bibtex] [pdf]
[43] Language-Based Defenses Against Untrusted Browser Origins (, and ), In Proceedings of the 22th USENIX Security Symposium, . [bibtex] [pdf]
[42] Secure distributed programming with value-dependent types (, , , , and ), In J. Funct. Program., volume 23, . [bibtex] [pdf]
[41] Implementing TLS with Verified Cryptographic Security (, , , and ), In IEEE Symposium on Security & Privacy (Oakland), . [bibtex] [pdf]
2012
[40] Web-based Attacks on Host-Proof Encrypted Storage ( and ), In 6th USENIX Workshop on Offensive Technologies (WOOT'12), . [bibtex] [pdf]
[39] Discovering Concrete Attacks on Website Authorization by Formal Analysis (, and ), In 25th IEEE Computer Security Foundations Symposium (CSF'12), . [bibtex] [pdf]
[38]Towards the Automated Verification of Cryptographic Protocol Implementations (), PhD thesis, École Normale Supérieure, . [bibtex]
[37] Verified Cryptographic Implementations for TLS (, , and ), In ACM Transactions Inf. Syst. Secur., ACM, volume 15, . [bibtex] [pdf]
2011
[36] Secure distributed programming with value-dependent types (, , , , and ), In 16th ACM SIGPLAN international conference on Functional Programming, . [bibtex] [pdf]
[35] Cryptographic Verification by Typing for a Sample Protocol Implementation (, and ), In Foundations of Security Analysis and Design VI (FOSAD'10), . [bibtex] [pdf]
[34] Refinement types for secure implementations (, , , and ), In ACM Trans. Program. Lang. Syst., volume 33, . [bibtex] [pdf]
2010
[33] Typechecking Higher-Order Security Libraries (, and ), In 8th Asian Symposium on Programming Languages and Systems, . [bibtex] [pdf]
[32] Modular verification of security protocol code by typing (, and ), In 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'10), . [bibtex] [pdf]
2009
[31] A compositional theory for STM Haskell (, and ), In 2nd ACM SIGPLAN Symposium on Haskell, . [bibtex] [pdf]
[30] Cryptographic Protocol Synthesis and Verification for Multiparty Sessions (, , , and ), In 22nd IEEE Computer Security Foundations Symposium (CSF-22), . [bibtex] [pdf]
2008
[29] A secure compiler for session abstractions (, , , and ), In Journal of Computer Security, volume 16, . [bibtex] [pdf]
[28] Service Combinators for Farming Virtual Machines (, and ), In 10th International Conference on Coordination Models and Languages, . [bibtex] [pdf]
[27] Verified interoperable implementations of security protocols (, , and ), In ACM Transactions on Programming Languages and Systems, volume 31, . [bibtex] [pdf]
[26] Verified implementations of the information card federated identity-management protocol (, , and ), In ACM Symposium on Information, Computer and Communications Security (ASIACCS), . [bibtex] [pdf]
[25] Verifying policy-based web services security (, and ), In ACM Transactions on Programming Languages and Systems, volume 30, . [bibtex] [pdf]
[24] Cryptographically verified implementations for TLS (, , and ), In ACM Conference on Computer and Communications Security, . [bibtex] [pdf]
[23] Refinement Types for Secure Implementations (, , , and ), In 21st IEEE Computer Security Foundations Symposium (CSF-21), . [bibtex] [pdf]
2007
[22]Service Combinators for Farming Virtual Machines (, and ), In Third Symposium on Trustworthy Global Computing (TGC), . [bibtex]
[21] Secure sessions for Web services (, , and ), In ACM Transactions on Information and System Security, volume 10, . [bibtex] [pdf]
2006
[20] Verified Interoperable Implementations of Security Protocols (, , and ), In 19th IEEE Computer Security Foundations Workshop (CSFW'06), . [bibtex] [pdf]
[19] Verified Reference Implementations of WS-Security Protocols (, and ), In Third International Workshop on Web Services and Formal Methods, . [bibtex] [pdf]
2005
[18] A Semantics for Web Services Authentication (, and ), In Theoretical Computer Science, Elsevier, volume 340, . [bibtex] [pdf]
[17] Network Event Recognition ( and ), In Formal Methods in System Design, volume 27, . [bibtex] [pdf]
[16] Brief announcement: exploring the consistency problem space (, and ), In Principles of Distributed Computing, . [bibtex] [pdf]
[15] An Advisor for Web Services Security Policies (, , and ), In 2005 ACM Workshop on Secure Web Services (SWS'05), ACM, . [bibtex] [pdf]
2004
[14] Verifying Policy-Based Security for Web Services (, and ), In 11th ACM Conference on Computer and Communications Security (CCS'04), . [bibtex] [pdf]
[13] Secure Sessions for Web Services (, , and ), In 2004 ACM Workshop on Secure Web Services (SWS'04), . [bibtex] [pdf]
[12] A Constraint-Based Formalism for Consistency in Replicated Systems (, and ), In 8th International Conference On Principles Of DIstributed Systems (OPODIS'04), . [bibtex] [pdf]
[11] TulaFale: A Security Tool for Web Services (, , and ), In International Symposium on Formal Methods for Components and Objects (FMCO'03), SV, volume 3188, . [bibtex] [pdf]
[10] A Semantics for Web Services Authentication (, and ), In 31st ACM Symposium on Principles of Programming Languages (POPL'04), . [bibtex] [pdf]
2003
[9] Network Event Recognition (), PhD thesis, University of Pennsylvania, . [bibtex] [pdf]
2002
[8] Verisim: Formal Analysis of Network Simulations (, , , , , and ), In IEEE Transactions on Software Engineering (TSE), volume 28, . [bibtex] [pdf]
[7] Formal verification of standards for distance vector routing protocols (, and ), In Journal of the ACM (JACM), volume 49, . [bibtex] [pdf]
[6] Requirements for a Practical Network Event Recognition Language ( and ), In Runtime Verification Workshop (RV'02), . [bibtex] [pdf]
2001
[5] What packets may come: automata for network monitoring (, , and ), In 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'01), . [bibtex] [pdf]
2000
[4] Routing Information Protocol in HOL/SPIN (, and ), In Theorem Proving in Higher-Order Logics (TPHOLs'00), . [bibtex] [pdf]
[3] Verisim: Formal analysis of network simulations (, , , , , and ), In ISSTA, . [bibtex] [pdf]
[2] Fault origin adjudication (, and ), In Third Workshop on Formal Methods in Software Practice (FMSP'00), . [bibtex] [pdf]
1998
[1] The Village Telephone System: A Case Study in Formal Software Engineering (, , , , and ), In Theorem Proving in Higher-Order Logics (TPHOLs'98), . [bibtex] [pdf]