Karthikeyan Bhargavan

120 papers A* 33A 14B 2C 2Misc 1Journal 43Unranked 25
YearRankTypeTitle / Venue / Authors
2025 J jnl
A Mechanically Verified Garbage Collector for OCaml.
J. Autom. Reason.
Sheera Shamsu, Dipesh Kafle, Dhruv Maroo, Kartik Nagar, Karthikeyan Bhargavan, K. C. Sivaramakrishnan
2025 A* conf
Formal Security and Functional Verification of Cryptographic Protocol Implementations in Rust.
CCS
Karthikeyan Bhargavan, Lasse Letager Hansen, Franziskus Kiefer, Jonas Schneider-Bensch, Bas Spitters
2025 J jnl
Formal Security and Functional Verification of Cryptographic Protocol Implementations in Rust.
IACR Cryptol. ePrint Arch.
Karthikeyan Bhargavan, Lasse Letager Hansen, Franziskus Kiefer, Jonas Schneider-Bensch, Bas Spitters
2025 J jnl
KyberSlash: Exploiting secret-dependent division timings in Kyber implementations.
IACR Trans. Cryptogr. Hardw. Embed. Syst.
Daniel J. Bernstein, Karthikeyan Bhargavan, Shivam Bhasin, Anupam Chattopadhyay, Tee Kiah Chia, Matthias J. Kannwischer, Franziskus Kiefer, Thales B. Paiva, Prasanna Ravi, Goutam Tamvada
2025 A* conf
TreeKEM: A Modular Machine-Checked Symbolic Security Analysis of Group Key Agreement in Messaging Layer Security.
SP
Théophile Wallez, Jonathan Protzenko, Karthikeyan Bhargavan
2025 J jnl
TreeKEM: A Modular Machine-Checked Symbolic Security Analysis of Group Key Agreement in Messaging Layer Security.
IACR Cryptol. ePrint Arch.
Théophile Wallez, Jonathan Protzenko, Karthikeyan Bhargavan
2025 J jnl
hax: Verifying Security-Critical Rust Software using Multiple Provers.
IACR Cryptol. ePrint Arch.
Karthikeyan Bhargavan, Maxime Buyse, Lucas Franceschino, Lasse Letager Hansen, Franziskus Kiefer, Jonas Schneider-Bensch, Bas Spitters
2024 A* conf
Formal verification of the PQXDH Post-Quantum key agreement protocol for end-to-end secure messaging.
USENIX Security Symposium
Karthikeyan Bhargavan, Charlie Jacomme, Franziskus Kiefer, Rolfe Schmidt
2024 J jnl
KyberSlash: Exploiting secret-dependent division timings in Kyber implementations.
IACR Cryptol. ePrint Arch.
Daniel J. Bernstein, Karthikeyan Bhargavan, Shivam Bhasin, Anupam Chattopadhyay, Tee Kiah Chia, Matthias J. Kannwischer, Franziskus Kiefer, Thales B. Paiva, Prasanna Ravi, Goutam Tamvada
2024 — conf
hax: Verifying Security-Critical Rust Software Using Multiple Provers.
VSTTE
Karthikeyan Bhargavan, Maxime Buyse, Lucas Franceschino, Lasse Letager Hansen, Franziskus Kiefer, Jonas Schneider-Bensch, Bas Spitters
2023 A* conf
Comparse: Provably Secure Formats for Cryptographic Protocols.
CCS
Théophile Wallez, Jonathan Protzenko, Karthikeyan Bhargavan
2023 J jnl
Comparse: Provably Secure Formats for Cryptographic Protocols.
IACR Cryptol. ePrint Arch.
Théophile Wallez, Jonathan Protzenko, Karthikeyan Bhargavan
2023 J jnl
Foundations of WebAssembly (Dagstuhl Seminar 23101).
Dagstuhl Reports
Karthikeyan Bhargavan, Jonathan Protzenko, Andreas Rossberg, Deian Stefan
2023 A conf
From Dragondoom to Dragonstar: Side-channel Attacks and Formally Verified Implementation of WPA3 Dragonfly Handshake.
EuroS&P
Daniel De Almeida Braga, Natalia Kulatova, Mohamed Sabt, Pierre-Alain Fouque, Karthikeyan Bhargavan
2023 J jnl
From Dragondoom to Dragonstar: Side-channel Attacks and Formally Verified Implementation of WPA3 Dragonfly Handshake.
CoRR
Daniel De Almeida Braga, Natalia Kulatova, Mohamed Sabt, Pierre-Alain Fouque, Karthikeyan Bhargavan
2023 — conf
Layered Symbolic Security Analysis in $\textsf {DY}^\star $.
ESORICS (3)
Karthikeyan Bhargavan, Abhishek Bichhawat, Pedram Hosseyni, Ralf Küsters, Klaas Pruiksma, Guido Schmitz, Clara Waldmann, Tim Würtele
2023 J jnl
Layered Symbolic Security Analysis in DY$^\star$.
IACR Cryptol. ePrint Arch.
Karthikeyan Bhargavan, Abhishek Bichhawat, Pedram Hosseyni, Ralf Küsters, Klaas Pruiksma, Guido Schmitz, Clara Waldmann, Tim Würtele
2023 A* conf
TreeSync: Authenticated Group Management for Messaging Layer Security.
USENIX Security Symposium
Théophile Wallez, Jonathan Protzenko, Benjamin Beurdouche, Karthikeyan Bhargavan
2022 A* conf
A Symbolic Analysis of Privacy for TLS 1.3 with Encrypted Client Hello.
CCS
Karthikeyan Bhargavan, Vincent Cheval, Christopher A. Wood
2022 J jnl
Hybrid Public Key Encryption.
RFC
Richard L. Barnes, Karthikeyan Bhargavan, Benjamin Lipp, Christopher A. Wood
2022 J jnl
Noise*: A Library of Verified High-Performance Secure Channel Protocol Implementations (Long Version).
IACR Cryptol. ePrint Arch.
Son Ho, Jonathan Protzenko, Abhishek Bichhawat, Karthikeyan Bhargavan
2022 A* conf
Noise*: A Library of Verified High-Performance Secure Channel Protocol Implementations.
SP
Son Ho, Jonathan Protzenko, Abhishek Bichhawat, Karthikeyan Bhargavan
2022 J jnl
TreeSync: Authenticated Group Management for Messaging Layer Security.
IACR Cryptol. ePrint Arch.
Théophile Wallez, Jonathan Protzenko, Benjamin Beurdouche, Karthikeyan Bhargavan
2021 — conf
A Tutorial-Style Introduction to DY*.
Protocols, Strands, and Logic
Karthikeyan Bhargavan, Abhishek Bichhawat, Quoc Huy Do, Pedram Hosseyni, Ralf Küsters, Guido Schmitz, Tim Würtele
2021 A* conf
An In-Depth Symbolic Security Analysis of the ACME Standard.
CCS
Karthikeyan Bhargavan, Abhishek Bichhawat, Quoc Huy Do, Pedram Hosseyni, Ralf Küsters, Guido Schmitz, Tim Würtele
2021 J jnl
An In-Depth Symbolic Security Analysis of the ACME Standard.
IACR Cryptol. ePrint Arch.
Karthikeyan Bhargavan, Abhishek Bichhawat, Quoc Huy Do, Pedram Hosseyni, Ralf Küsters, Guido Schmitz, Tim Würtele
2021 A conf
DY*: A Modular Symbolic Verification Framework for Executable Cryptographic Protocol Code.
EuroS&P
Karthikeyan Bhargavan, Abhishek Bichhawat, Quoc Huy Do, Pedram Hosseyni, Ralf Küsters, Guido Schmitz, Tim Würtele
2020 A* conf
EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider.
SP
Jonathan Protzenko, Bryan Parno, Aymeric Fromherz, Chris Hawblitzel, Marina Polubelova, Karthikeyan Bhargavan, Benjamin Beurdouche, Joonwon Choi, Antoine Delignat-Lavaud, Cédric Fournet, Natalia Kulatova, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Christoph M. Wintersteiger, Santiago Zanella-Béguelin
2020 A* conf
HACLxN: Verified Generic SIMD Crypto (for all your favourite platforms).
CCS
Marina Polubelova, Karthikeyan Bhargavan, Jonathan Protzenko, Benjamin Beurdouche, Aymeric Fromherz, Natalia Kulatova, Santiago Zanella-Béguelin
2020 J jnl
HACL×N: Verified Generic SIMD Crypto (for all your favorite platforms).
IACR Cryptol. ePrint Arch.
Marina Polubelova, Karthikeyan Bhargavan, Jonathan Protzenko, Benjamin Beurdouche, Aymeric Fromherz, Natalia Kulatova, Santiago Zanella-Béguelin
2020 Misc ed.
Progress in Cryptology - INDOCRYPT 2020 - 21st International Conference on Cryptology in India, Bangalore, India, December 13-16, 2020, Proceedings
INDOCRYPT
Karthikeyan Bhargavan, Elisabeth Oswald, Manoj Prabhakaran
2019 A conf
A Mechanised Cryptographic Proof of the WireGuard Virtual Private Network Protocol.
EuroS&P
Benjamin Lipp, Bruno Blanchet, Karthikeyan Bhargavan
2019 J jnl
EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider.
IACR Cryptol. ePrint Arch.
Jonathan Protzenko, Bryan Parno, Aymeric Fromherz, Chris Hawblitzel, Marina Polubelova, Karthikeyan Bhargavan, Benjamin Beurdouche, Joonwon Choi, Antoine Delignat-Lavaud, Cédric Fournet, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Christoph M. Wintersteiger, Santiago Zanella-Béguelin
2019 A* conf
Formally Verified Cryptographic Web Applications in WebAssembly.
IEEE Symposium on Security and Privacy
Jonathan Protzenko, Benjamin Beurdouche, Denis Merigoux, Karthikeyan Bhargavan
2019 J jnl
Formally Verified Cryptographic Web Applications in WebAssembly.
IACR Cryptol. ePrint Arch.
Jonathan Protzenko, Benjamin Beurdouche, Denis Merigoux, Karthikeyan Bhargavan
2019 J jnl
Imperfect forward secrecy: how Diffie-Hellman fails in practice.
Commun. ACM
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, Paul Zimmermann
2019 A conf
Noise Explorer: Fully Automated Modeling and Verification for Arbitrary Noise Protocols.
EuroS&P
Nadim Kobeissi, Georgio Nicolas, Karthikeyan Bhargavan
2019 — conf
Practical Formal Methods for Real World Cryptography (Invited Talk).
FSTTCS
Karthikeyan Bhargavan, Prasad Naldurg
2019 J jnl
SoK: Computer-Aided Cryptography.
IACR Cryptol. ePrint Arch.
Manuel Barbosa, Gilles Barthe, Karthikeyan Bhargavan, Bruno Blanchet, Cas Cremers, Kevin Liao, Bryan Parno
2018 A* conf
A Formal Treatment of Accountable Proxying Over TLS.
IEEE Symposium on Security and Privacy
Karthikeyan Bhargavan, Ioana Boureanu, Antoine Delignat-Lavaud, Pierre-Alain Fouque, Cristina Onete
2018 J jnl
Noise Explorer: Fully Automated Modeling and Verification for Arbitrary Noise Protocols.
IACR Cryptol. ePrint Arch.
Nadim Kobeissi, Karthikeyan Bhargavan
2018 — conf
hacspec: Towards Verifiable Crypto Standards.
SSR
Karthikeyan Bhargavan, Franziskus Kiefer, Pierre-Yves Strub
2017 J jnl
A messy state of the union: taming the composite state machines of TLS.
Commun. ACM
Benjamin Beurdouche, Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub, Jean Karim Zinzindohoue
2017 A conf
Automated Verification for Secure Messaging Protocols and Their Implementations: A Symbolic and Computational Approach.
EuroS&P
Nadim Kobeissi, Karthikeyan Bhargavan, Bruno Blanchet
2017 A conf
Content delivery over TLS: a cryptographic analysis of keyless SSL.
EuroS&P
Karthikeyan Bhargavan, Ioana Boureanu, Pierre-Alain Fouque, Cristina Onete, Benjamin Richard
2017 — conf
Everest: Towards a Verified, Drop-in Replacement of HTTPS.
SNAPL
Karthikeyan Bhargavan, Barry Bond, Antoine Delignat-Lavaud, Cédric Fournet, Chris Hawblitzel, Catalin Hritcu, Samin Ishtiaq, Markulf Kohlweiss, K. Rustan M. 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
2017 — conf
Formal Modeling and Verification for Domain Validation and ACME.
Financial Cryptography
Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Nadim Kobeissi
2017 A* conf
HACL*: A Verified Modern Cryptographic Library.
CCS
Jean Karim Zinzindohoué, Karthikeyan Bhargavan, Jonathan Protzenko, Benjamin Beurdouche
2017 J jnl
HACL*: A Verified Modern Cryptographic Library.
IACR Cryptol. ePrint Arch.
Jean Karim Zinzindohoué, Karthikeyan Bhargavan, Jonathan Protzenko, Benjamin Beurdouche
2017 A* conf
Implementing and Proving the TLS 1.3 Record Layer.
IEEE Symposium on Security and Privacy
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
2017 J jnl
Verified Low-Level Programming Embedded in F
CoRR
Jonathan Protzenko, Jean Karim Zinzindohoué, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella-Béguelin, Antoine Delignat-Lavaud, Catalin Hritcu, Karthikeyan Bhargavan, Cédric Fournet, Nikhil Swamy
2017 A* conf
Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate.
IEEE Symposium on Security and Privacy
Karthikeyan Bhargavan, Bruno Blanchet, Nadim Kobeissi
2017 J jnl
Verified low-level programming embedded in F.
Proc. ACM Program. Lang.
Jonathan Protzenko, Jean Karim Zinzindohoué, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella-Béguelin, Antoine Delignat-Lavaud, Catalin Hritcu, Karthikeyan Bhargavan, Cédric Fournet, Nikhil Swamy
2016 A conf
A Verified Extensible Library of Elliptic Curves.
CSF
Jean Karim Zinzindohoue, Evmorfia-Iro Bartzia, Karthikeyan Bhargavan
2016 A* conf
Dependent types and multi-monadic effects in F.
POPL
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
2016 A* conf
Downgrade Resilience in Key-Exchange Protocols.
IEEE Symposium on Security and Privacy
Karthikeyan Bhargavan, Christina Brzuska, Cédric Fournet, Matthew Green, Markulf Kohlweiss, Santiago Zanella-Béguelin
2016 J jnl
Downgrade Resilience in Key-Exchange Protocols.
IACR Cryptol. ePrint Arch.
Karthikeyan Bhargavan, Christina Brzuska, Cédric Fournet, Matthew Green, Markulf Kohlweiss, Santiago Zanella-Béguelin
2016 — conf
Formal Verification of Smart Contracts: Short Paper.
PLAS@CCS
Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Anitha Gollamudi, Georges Gonthier, Nadim Kobeissi, Natalia Kulatova, Aseem Rastogi, Thomas Sibut-Pinote, Nikhil Swamy, Santiago Zanella-Béguelin
2016 J jnl
Implementing and Proving the TLS 1.3 Record Layer.
IACR Cryptol. ePrint Arch.
Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Jianyang Pan, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy, Santiago Zanella-Béguelin, Jean Karim Zinzindohoue
2016 A* conf
On the Practical (In-)Security of 64-bit Block Ciphers: Collision Attacks on HTTP over TLS and OpenVPN.
CCS
Karthikeyan Bhargavan, Gaëtan Leurent
2016 J jnl
On the Practical (In-)Security of 64-bit Block Ciphers: Collision Attacks on HTTP over TLS and OpenVPN.
IACR Cryptol. ePrint Arch.
Karthikeyan Bhargavan, Gaëtan Leurent
2016 A* conf
Transcript Collision Attacks: Breaking Authentication in TLS, IKE and SSH.
NDSS
Karthikeyan Bhargavan, Gaëtan Leurent
2016 J jnl
miTLS: Verifying Protocol Implementations against Real-World Attacks.
IEEE Secur. Priv.
Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss
2015 A* conf
A Messy State of the Union: Taming the Composite State Machines of TLS.
IEEE Symposium on Security and Privacy
Benjamin Beurdouche, Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub, Jean Karim Zinzindohoue
2015 — conf
FLEXTLS: A Tool for Testing TLS Implementations.
WOOT
Benjamin Beurdouche, Antoine Delignat-Lavaud, Nadim Kobeissi, Alfredo Pironti, Karthikeyan Bhargavan
2015 A* conf
Imperfect Forward Secrecy: How Diffie-Hellman Fails in Practice.
CCS
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, Paul Zimmermann
2015 A* conf
Network-based Origin Confusion Attacks against HTTPS Virtual Hosting.
WWW
Antoine Delignat-Lavaud, Karthikeyan Bhargavan
2015 J jnl
Transport Layer Security (TLS) Session Hash and Extended Master Secret Extension.
RFC
Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Alfredo Pironti, Adam Langley, Marsh Ray
2015 A* conf
Verified Contributive Channel Bindings for Compound Authentication.
NDSS
Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Alfredo Pironti
2014 J jnl
Discovering concrete attacks on website authorization by formal analysis.
J. Comput. Secur.
Chetan Bansal, Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Sergio Maffeis
2014 A* conf
Gradual typing embedded securely in JavaScript.
POPL
Nikhil Swamy, Cédric Fournet, Aseem Rastogi, Karthikeyan Bhargavan, Juan Chen, Pierre-Yves Strub, Gavin M. Bierman
2014 — conf
Proving the TLS Handshake Secure (As It Is).
CRYPTO (2)
Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub, Santiago Zanella-Béguelin
2014 J jnl
Proving the TLS Handshake Secure (as it is).
IACR Cryptol. ePrint Arch.
Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub, Santiago Zanella-Béguelin
2014 A* conf
Triple Handshakes and Cookie Cutters: Breaking and Fixing Authentication over TLS.
IEEE Symposium on Security and Privacy
Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Alfredo Pironti, Pierre-Yves Strub
2013 — conf
Defensive JavaScript - Building and Verifying Secure Web Components.
FOSAD
Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Sergio Maffeis
2013 A* conf
Implementing TLS with Verified Cryptographic Security.
IEEE Symposium on Security and Privacy
Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub
2013 — conf
Keys to the Cloud: Formal Analysis and Concrete Attacks on Encrypted Web Storage.
POST
Chetan Bansal, Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Sergio Maffeis
2013 A* conf
Language-based Defenses Against Untrusted Browser Origins.
USENIX Security Symposium
Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Sergio Maffeis
2013 J jnl
Secure distributed programming with value-dependent types.
J. Funct. Program.
Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, Jean Yang
2013 — conf
Towards Unified Authorization for Android.
ESSoS
Michael J. May, Karthikeyan Bhargavan
2012 A conf
Discovering Concrete Attacks on Website Authorization by Formal Analysis.
CSF
Chetan Bansal, Karthikeyan Bhargavan, Sergio Maffeis
2012 J jnl
Verified Cryptographic Implementations for TLS.
ACM Trans. Inf. Syst. Secur.
Karthikeyan Bhargavan, Cédric Fournet, Ricardo Corin, Eugen Zalinescu
2012 — conf
Web-based Attacks on Host-Proof Encrypted Storage.
WOOT
Karthikeyan Bhargavan, Antoine Delignat-Lavaud
2011 — conf
Cryptographic Verification by Typing for a Sample Protocol Implementation.
FOSAD
Cédric Fournet, Karthikeyan Bhargavan, Andrew D. Gordon
2011 J jnl
Refinement types for secure implementations.
ACM Trans. Program. Lang. Syst.
Jesper Bengtson, Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Sergio Maffeis
2011 A conf
Secure distributed programming with value-dependent types.
ICFP
Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, Jean Yang
2010 A* conf
Modular verification of security protocol code by typing.
POPL
Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon
2010 B conf
Typechecking Higher-Order Security Libraries.
APLAS
Karthikeyan Bhargavan, Cédric Fournet, Nataliya Guts
2009 C conf
A compositional theory for STM Haskell.
Haskell
Johannes Borgström, Karthikeyan Bhargavan, Andrew D. Gordon
2009 A conf
Cryptographic Protocol Synthesis and Verification for Multiparty Sessions.
CSF
Karthikeyan Bhargavan, Ricardo Corin, Pierre-Malo Deniélou, Cédric Fournet, James J. Leifer
2008 J jnl
A secure compiler for session abstractions.
J. Comput. Secur.
Ricardo Corin, Pierre-Malo Deniélou, Cédric Fournet, Karthikeyan Bhargavan, James J. Leifer
2008 A* conf
Cryptographically verified implementations for TLS.
CCS
Karthikeyan Bhargavan, Cédric Fournet, Ricardo Corin, Eugen Zalinescu
2008 A conf
Refinement Types for Secure Implementations.
CSF
Jesper Bengtson, Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Sergio Maffeis
2008 C conf
Service Combinators for Farming Virtual Machines.
COORDINATION
Karthikeyan Bhargavan, Andrew D. Gordon, Iman Narasamdya
2008 A conf
Verified implementations of the information card federated identity-management protocol.
AsiaCCS
Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Nikhil Swamy
2008 J jnl
Verified interoperable implementations of security protocols.
ACM Trans. Program. Lang. Syst.
Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Stephen Tse
2008 J jnl
Verifying policy-based web services security.
ACM Trans. Program. Lang. Syst.
Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon
2007 A conf
Secure Implementations for Typed Session Abstractions.
CSF
Ricardo Corin, Pierre-Malo Deniélou, Cédric Fournet, Karthikeyan Bhargavan, James J. Leifer
2007 J jnl
Secure sessions for Web services.
ACM Trans. Inf. Syst. Secur.
Karthikeyan Bhargavan, Ricardo Corin, Cédric Fournet, Andrew D. Gordon
2007 — conf
Service Combinators for Farming Virtual Machines.
TGC
Karthikeyan Bhargavan, Andrew D. Gordon, Iman Narasamdya
2006 — conf
Verified Interoperable Implementations of Security Protocols.
CSFW
Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Stephen Tse
2006 — conf
Verified Reference Implementations of WS-Security Protocols.
WS-FM
Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon
2005 J jnl
A semantics for web services authentication.
Theor. Comput. Sci.
Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon
2005 — conf
An advisor for web services security policies.
SWS
Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Greg O'Shea
2005 A* conf
Brief announcement: exploring the consistency problem space.
PODC
Nishith Krishna, Marc Shapiro, Karthikeyan Bhargavan
2005 J jnl
Network Event Recognition.
Formal Methods Syst. Des.
Karthikeyan Bhargavan, Carl A. Gunter
2004 B conf
A Constraint-Based Formalism for Consistency in Replicated Systems.
OPODIS
Marc Shapiro, Karthikeyan Bhargavan, Nishith Krishna
2004 A* conf
A semantics for web services authentication.
POPL
Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon
2004 — conf
Secure sessions for web services.
SWS
Karthikeyan Bhargavan, Ricardo Corin, Cédric Fournet, Andrew D. Gordon
2004 J jnl
TulaFale: A Security Tool for Web Services
CoRR
Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Riccardo Pucella
2004 A* conf
Verifying policy-based security for web services.
CCS
Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon
2003 — conf
TulaFale: A Security Tool for Web Services.
FMCO
Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Riccardo Pucella
2002 J jnl
Formal verification of standards for distance vector routing protocols.
J. ACM
Karthikeyan Bhargavan, Davor Obradovic, Carl A. Gunter
2002 — conf
Requirements for a Practical Network Event Recognition Language.
RV@FLoC
Karthikeyan Bhargavan, Carl A. Gunter
2002 J jnl
Verisim: Formal Analysis of Network Simulations.
IEEE Trans. Software Eng.
Karthikeyan Bhargavan, Carl A. Gunter, Moonjoo Kim, Insup Lee, Davor Obradovic, Oleg Sokolsky, Mahesh Viswanathan
2001 A* conf
What packets may come: automata for network monitoring.
POPL
Karthikeyan Bhargavan, Satish Chandra, Peter J. McCann, Carl A. Gunter
2000 — conf
Fault origin adjudication.
FMSP
Karthikeyan Bhargavan, Carl A. Gunter, Davor Obradovic
2000 — conf
Routing Information Protocol in HOL/SPIN.
TPHOLs
Karthikeyan Bhargavan, Carl A. Gunter, Davor Obradovic
2000 A conf
Verisim: Formal analysis of network simulations.
ISSTA
Karthikeyan Bhargavan, Carl A. Gunter, Moonjoo Kim, Insup Lee, Davor Obradovic, Oleg Sokolsky, Mahesh Viswanathan
1998 — conf
The Village Telephone System: A Case Study in Formal Software Engineering.
TPHOLs
Karthikeyan Bhargavan, Carl A. Gunter, Elsa L. Gunter, Michael Jackson, Davor Obradovic, Pamela Zave