2017
[69] Automated Verification for Secure Messaging Protocols and their Implementations: A Symbolic and Computational Approach (N. Kobeissi, K. Bhargavan, B. Blanchet), In IEEE European Symposium on Security and Privacy (EuroS&P), 2017. (to appear) [bib]
[68] Content delivery over TLS: a cryptographic analysis of Keyless SSL (I. Carlson P. Fouque C. Onete B. Richard K. Bhargavan), In IEEE European Symposium on Security and Privacy (EuroS&P), 2017. (to appear) [bib]
[67] Formal Modeling and Verification for Domain Validation and ACME (Antoine Delignat-Lavaud Karthikeyan Bhargavan, Nadim Kobeissi), In Financial Cryptography and Data Security (FC), 2017. (to appear) [bib]
[66] Implementing and Proving the TLS 1.3 Record Layer (Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy, Santiago Zanella Béguelin, Karthikeyan Bhargavan, Jianyang Pan, Jean Karim Zinzindohoue), In 2017 IEEE Symposium on Security and Privacy, SP 2017, San Jose, CA, USA, May 22-26, 2017, 2017. [bib] [pdf] [doi]
[65] Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate (Karthikeyan Bhargavan, Bruno Blanchet, Nadim Kobeissi), In 2017 IEEE Symposium on Security and Privacy, SP 2017, San Jose, CA, USA, May 22-26, 2017, 2017. [bib] [pdf] [doi]
[64] Everest: Towards a Verified, Drop-in Replacement of HTTPS (Karthikeyan Bhargavan, Barry Bond, Antoine Delignat-Lavaud, Cédric Fournet, Chris Hawblitzel, Catalin Hritcu, Samin Ishtiaq, Markulf Kohlweiss, Rustan Leino, Jay R. Lorch, Kenji Maillard, Jianyang Pan, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Ashay Rane, Aseem Rastogi, Nikhil Swamy, Laure Thompson, Peng Wang, Santiago Zanella Béguelin, Jean Karim Zinzindohoue), In 2nd Summit on Advances in Programming Languages, SNAPL 2017, May 7-10, 2017, Asilomar, CA, USA, 2017. [bib] [pdf] [doi]
[63] 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 Communications of the ACM, volume 60, 2017. [bib]
2016
[62] miTLS: Verifying Protocol Implementations against Real-World Attacks (K. Bhargavan, C. Fournet, M. Kohlweiss), In IEEE Security & Privacy Magazine, volume 14, 2016. [bib]
[61] Dependent Types and Multi-Monadic Effects in F* (Nikhil Swamy, Catalin Hritcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoue, Santiago Zanella-Béguelin), In 43nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 2016. [bib] [pdf]
[60] A Verified Extensible Library of Elliptic Curves (Jean Karim Zinzindohoue, Evmorfia-Iro Bartzia, Karthikeyan Bhargavan), In IEEE Computer Security Foundations Symposium (CSF), 2016. [bib]
[59] Transcript Collision Attacks: Breaking Authentication in TLS, IKE, and SSH (Karthikeyan Bhargavan, Gaetan Leurent), In Proceedings of the ISOC Network and Distributed System Security Symposium (NDSS '16), 2016. (Distinguished paper award) [bib] [pdf]
[58] Downgrade Resilience in Key-Exchange Protocols (Karthikeyan Bhargavan, Christina Brzuska, Cédric Fournet, Matthew Green, Markulf Kohlweiss, Santiago Zanella-Béguelin), In IEEE Symposium on Security & Privacy (Oakland), 2016. [bib]
[57] ProScript-TLS: Verifiable Models and Systematic Testing for TLS 1.3 (Karthikeyan Bhargavan, Nadim Kobeissi), 2016. (Presented at the TRON workshop) [bib] [pdf]
[56] On the Practical (In-)Security of 64-bit Block Ciphers (Karthikeyan Bhargavan, Gaëtan Leurent), In ACM Conference on Computer and Communications Security (CCS'16), 2016. [bib] [pdf]
2015
[55] 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]
[54] Network-based Origin Confusion Attacks against HTTPS Virtual Hosting (Antoine Delignat-Lavaud, Karthikeyan Bhargavan), In International Conference on World Wide Web (WWW'15), 2015. [bib] [pdf]
[53] Verified Contributive Channel Bindings for Compound Authentication (Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Alfredo Pironti), In Network and Distributed System Security Symposium (NDSS '15), 2015. [bib] [pdf]
[52] Imperfect Forward Secrecy: How Diffie-Hellman Fails in Practice (David Adrian, Karthikeyan Bhargavan, Zakir Durumeric, Pierrick Gaudry, Matthew Green, J. Alex Halderman, Nadia Heninger, Drew Springall, Emmanuel Thomé, Luke Valenta, Benjamin VanderSloot, Eric Wustrow, Santiago Zanella-Béguelin, and Paul Zimmermann), In ACM Conference on Computer and Communications Security (CCS'15), 2015. (Best student paper award) [bib] [pdf]
[51] FLEXTLS: A Tool for Testing TLS Implementations (Benjamin Beurdouche, Antoine Delignat-Lavaud, Nadim Kobeissi, Alfredo Pironti, Karthikeyan Bhargavan), In USENIX Workshop on Offensive Technologies (WOOT'15), 2015. (Best Paper Award) [bib] [pdf]
2014
[50] Proving the TLS Handshake Secure (as it is) (Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub, Santiago Zanella-Béguelin), In CRYPTO, 2014. (Long version at Cryptology ePrint Archive, Report 2014/182: https://eprint.iacr.org/2014/182) [bib]
[49] Gradual typing embedded securely in JavaScript (Nikhil Swamy, Cédric Fournet, Aseem Rastogi, Karthikeyan Bhargavan, Juan Chen, Pierre-Yves Strub, Gavin M. Bierman), In The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '14), 2014. [bib] [pdf]
[48] Defensive JavaScript - Building and Verifying Secure Web Components (Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Sergio Maffeis), Chapter in Foundations of Security Analysis and Design VII, FOSAD Tutorial Lectures, Springer Verlag, volume 8604, 2014. [bib] [pdf]
[47] Triple Handshakes and Cookie Cutters: Breaking and Fixing Authentication over TLS (Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, and Alfredo Pironti, Pierre-Yves Strub), In IEEE Symposium on Security & Privacy (Oakland), 2014. [bib] [pdf]
[46] Discovering concrete attacks on website authorization by formal analysis (Chetan Bansal, Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Sergio Maffeis), In Journal of Computer Security, volume 22, 2014. [bib] [pdf]
2013
[45] Towards Unified Authorization for Android (Michael J. May, Karthikeyan Bhargavan), In 5th International Symposium on Engineering Secure Software and Systems (ESSoS 2013), 2013. [bib] [pdf]
[44] Language-Based Defenses Against Untrusted Browser Origins (Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Sergio Maffeis), In Proceedings of the 22th USENIX Security Symposium, 2013. [bib] [pdf]
[43] Secure distributed programming with value-dependent types (Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, Jean Yang), In J. Funct. Program., volume 23, 2013. [bib] [pdf]
[42] Implementing TLS with Verified Cryptographic Security (Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub), In IEEE Symposium on Security & Privacy (Oakland), 2013. [bib] [pdf]
[41] Keys to the Cloud: Formal Analysis and Concrete Attacks on Encrypted Web Storage (Chetan Bansal, Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Sergio Maffeis), In 2nd Conference on Principles of Security and Trust (POST 2013) (David Basin, John Mitchell, eds.), Springer Verlag, 2013. [bib] [pdf]
2012
[40] Towards the Automated Verification of Cryptographic Protocol Implementations (Karthikeyan Bhargavan), 2012. (Mémoire d'habilitation) [bib]
[39] Verified Cryptographic Implementations for TLS (Karthikeyan Bhargavan, Cédric Fournet, Ricardo Corin, Eugen Zalinescu), In ACM Transactions Inf. Syst. Secur., ACM, volume 15, 2012. [bib] [pdf]
[38] Web-based Attacks on Host-Proof Encrypted Storage (Karthikeyan Bhargavan, Antoine Delignat-Lavaud), In 6th USENIX Workshop on Offensive Technologies (WOOT'12), 2012. [bib] [pdf]
[37] Discovering Concrete Attacks on Website Authorization by Formal Analysis (Chetan Bansal, Karthikeyan Bhargavan, Sergio Maffeis), In 25th IEEE Computer Security Foundations Symposium (CSF'12), 2012. [bib] [pdf]
2011
[36] Secure distributed programming with value-dependent types (Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, Jean Yang), In 16th ACM SIGPLAN international conference on Functional Programming, 2011. [bib] [pdf]
[35] Cryptographic Verification by Typing for a Sample Protocol Implementation (Cédric Fournet, Karthikeyan Bhargavan, Andrew D. Gordon), In Foundations of Security Analysis and Design VI (FOSAD'10), 2011. [bib] [pdf]
[34] Refinement types for secure implementations (Jesper Bengtson, Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Sergio Maffeis), In ACM Trans. Program. Lang. Syst., volume 33, 2011. [bib] [pdf]
2010
[33] Typechecking Higher-Order Security Libraries (Karthikeyan Bhargavan, Cédric Fournet, Nataliya Guts), In 8th Asian Symposium on Programming Languages and Systems, 2010. [bib] [pdf]
[32] Modular verification of security protocol code by typing (Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon), In 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'10), 2010. [bib] [pdf]
2009
[31] A compositional theory for STM Haskell (Johannes Borgström, Karthikeyan Bhargavan, Andrew D. Gordon), In 2nd ACM SIGPLAN Symposium on Haskell, 2009. [bib] [pdf]
[30] Cryptographic Protocol Synthesis and Verification for Multiparty Sessions (Karthikeyan Bhargavan, Ricardo Corin, Pierre-Malo Deniélou, Cédric Fournet, James J. Leifer), In 22nd IEEE Computer Security Foundations Symposium (CSF-22), 2009. [bib] [pdf]
2008
[29] A secure compiler for session abstractions (Ricardo Corin, Pierre-Malo Deniélou, Cédric Fournet, Karthikeyan Bhargavan, James J. Leifer), In Journal of Computer Security, volume 16, 2008. [bib] [pdf]
[28] Service Combinators for Farming Virtual Machines (Karthikeyan Bhargavan, Andrew D. Gordon, Iman Narasamdya), In 10th International Conference on Coordination Models and Languages, 2008. [bib] [pdf]
[27] Verified interoperable implementations of security protocols (Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Stephen Tse), In ACM Transactions on Programming Languages and Systems, volume 31, 2008. [bib] [pdf]
[26] Verified implementations of the information card federated identity-management protocol (Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Nikhil Swamy), In ACM Symposium on Information, Computer and Communications Security (ASIACCS), 2008. [bib] [pdf]
[25] Verifying policy-based web services security (Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon), In ACM Transactions on Programming Languages and Systems, volume 30, 2008. [bib] [pdf]
[24] Cryptographically verified implementations for TLS (Karthikeyan Bhargavan, Cédric Fournet, Ricardo Corin, Eugen Zalinescu), In ACM Conference on Computer and Communications Security, 2008. [bib] [pdf]
[23] Refinement Types for Secure Implementations (Jesper Bengtson, Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Sergio Maffeis), In 21st IEEE Computer Security Foundations Symposium (CSF-21), 2008. [bib] [pdf]
2007
[22] Service Combinators for Farming Virtual Machines (Karthikeyan Bhargavan, Andrew D. Gordon, Iman Narasamdya), In Third Symposium on Trustworthy Global Computing (TGC), 2007. [bib]
[21] Secure sessions for Web services (Karthikeyan Bhargavan, Ricardo Corin, Cédric Fournet, Andrew D. Gordon), In ACM Transactions on Information and System Security, volume 10, 2007. [bib] [pdf]
2006
[20] Verified Reference Implementations of WS-Security Protocols (Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon), In Third International Workshop on Web Services and Formal Methods, 2006. [bib] [pdf]
[19] Verified Interoperable Implementations of Security Protocols (Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Stephen Tse), In 19th IEEE Computer Security Foundations Workshop (CSFW'06), 2006. [bib] [pdf]
2005
[18] A Semantics for Web Services Authentication (Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon), In Theoretical Computer Science, Elsevier, volume 340, 2005. [bib] [pdf]
[17] Network Event Recognition (Karthikeyan Bhargavan, Carl A. Gunter), In Formal Methods in System Design, volume 27, 2005. [bib] [pdf]
[16] Brief announcement: exploring the consistency problem space (Nishith Krishna, Marc Shapiro, Karthikeyan Bhargavan), In Principles of Distributed Computing, 2005. [bib] [pdf]
[15] An Advisor for Web Services Security Policies (Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Greg O'Shea), In 2005 ACM Workshop on Secure Web Services (SWS'05), ACM, 2005. [bib] [pdf]
2004
[14] A Constraint-Based Formalism for Consistency in Replicated Systems (Marc Shapiro, Karthikeyan Bhargavan, Nishith Krishna), In 8th International Conference On Principles Of DIstributed Systems (OPODIS'04), 2004. [bib] [pdf]
[13] TulaFale: A Security Tool for Web Services (Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Riccardo Pucella), In International Symposium on Formal Methods for Components and Objects (FMCO'03), SV, volume 3188, 2004. [bib] [pdf]
[12] Verifying Policy-Based Security for Web Services (Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon), In 11th ACM Conference on Computer and Communications Security (CCS'04), 2004. [bib] [pdf]
[11] A Semantics for Web Services Authentication (Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon), In 31st ACM Symposium on Principles of Programming Languages (POPL'04), 2004. [bib] [pdf]
[10] Secure Sessions for Web Services (Karthikeyan Bhargavan, Ricardo Corin, Cédric Fournet, Andrew D. Gordon), In 2004 ACM Workshop on Secure Web Services (SWS'04), 2004. [bib] [pdf]
2003
[9] Network Event Recognition (Karthikeyan Bhargavan), 2003. [bib] [pdf]
2002
[8] Verisim: Formal Analysis of Network Simulations (Karthikeyan Bhargavan, Carl A. Gunter, Moonjoo Kim, Insup Lee, Davor Obradovic, Oleg Sokolsky, Mahesh Viswanathan), In IEEE Transactions on Software Engineering (TSE), volume 28, 2002. [bib] [pdf]
[7] 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]
[6] Requirements for a Practical Network Event Recognition Language (Karthikeyan Bhargavan, Carl A. Gunter), In Runtime Verification Workshop (RV'02), 2002. [bib] [pdf]
2001
[5] What packets may come: automata for network monitoring (Karthikeyan Bhargavan, Satish Chandra, Peter J. McCann, Carl A. Gunter), In 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'01), 2001. [bib] [pdf]
2000
[4] Routing Information Protocol in HOL/SPIN (Karthikeyan Bhargavan, Carl A. Gunter, Davor Obradovic), In Theorem Proving in Higher-Order Logics (TPHOLs'00), 2000. [bib] [pdf]
[3] Verisim: Formal analysis of network simulations (Karthikeyan Bhargavan, Carl A. Gunter, Moonjoo Kim, Insup Lee, Davor Obradovic, Oleg Sokolsky, Mahesh Viswanathan), In ISSTA, 2000. [bib] [pdf]
[2] Fault origin adjudication (Karthikeyan Bhargavan, Carl A. Gunter, Davor Obradovic), In Third Workshop on Formal Methods in Software Practice (FMSP'00), 2000. [bib] [pdf]
1998
[1] The Village Telephone System: A Case Study in Formal Software Engineering (Karthikeyan Bhargavan, Carl A. Gunter, Elsa L. Gunter, Michael Jackson, Davor Obradovic, Pamela Zave), In Theorem Proving in Higher-Order Logics (TPHOLs'98), 1998. [bib] [pdf]