


default search action
Karthikeyan Bhargavan
Karthik Bhargavan
Person information
- affiliation: INRIA, France
Refine list

refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2024
- [c74]Karthikeyan Bhargavan, Charlie Jacomme, Franziskus Kiefer, Rolfe Schmidt:
Formal verification of the PQXDH Post-Quantum key agreement protocol for end-to-end secure messaging. USENIX Security Symposium 2024 - [i22]Daniel J. Bernstein, Karthikeyan Bhargavan, Shivam Bhasin, Anupam Chattopadhyay, Tee Kiah Chia, Matthias J. Kannwischer, Franziskus Kiefer, Thales Paiva, Prasanna Ravi, Goutam Tamvada:
KyberSlash: Exploiting secret-dependent division timings in Kyber implementations. IACR Cryptol. ePrint Arch. 2024: 1049 (2024) - 2023
- [c73]Théophile Wallez
, Jonathan Protzenko
, Karthikeyan Bhargavan
:
Comparse: Provably Secure Formats for Cryptographic Protocols. CCS 2023: 564-578 - [c72]Karthikeyan Bhargavan
, Abhishek Bichhawat
, Pedram Hosseyni
, Ralf Küsters
, Klaas Pruiksma
, Guido Schmitz
, Clara Waldmann
, Tim Würtele
:
Layered Symbolic Security Analysis in $\textsf {DY}^\star $. ESORICS (3) 2023: 3-21 - [c71]Daniel De Almeida Braga
, Natalia Kulatova, Mohamed Sabt, Pierre-Alain Fouque
, Karthikeyan Bhargavan:
From Dragondoom to Dragonstar: Side-channel Attacks and Formally Verified Implementation of WPA3 Dragonfly Handshake. EuroS&P 2023: 707-723 - [c70]Théophile Wallez, Jonathan Protzenko, Benjamin Beurdouche, Karthikeyan Bhargavan:
TreeSync: Authenticated Group Management for Messaging Layer Security. USENIX Security Symposium 2023: 1217-1233 - [i21]Daniel De Almeida Braga, Natalia Kulatova, Mohamed Sabt, Pierre-Alain Fouque, Karthikeyan Bhargavan:
From Dragondoom to Dragonstar: Side-channel Attacks and Formally Verified Implementation of WPA3 Dragonfly Handshake. CoRR abs/2307.09243 (2023) - [i20]Karthikeyan Bhargavan, Jonathan Protzenko, Andreas Rossberg, Deian Stefan:
Foundations of WebAssembly (Dagstuhl Seminar 23101). Dagstuhl Reports 13(3): 1-16 (2023) - [i19]Karthikeyan Bhargavan, Abhishek Bichhawat, Pedram Hosseyni, Ralf Küsters, Klaas Pruiksma, Guido Schmitz, Clara Waldmann, Tim Würtele:
Layered Symbolic Security Analysis in DY$^\star$. IACR Cryptol. ePrint Arch. 2023: 1329 (2023) - [i18]Théophile Wallez, Jonathan Protzenko, Karthikeyan Bhargavan:
Comparse: Provably Secure Formats for Cryptographic Protocols. IACR Cryptol. ePrint Arch. 2023: 1390 (2023) - 2022
- [c69]Karthikeyan Bhargavan, Vincent Cheval, Christopher A. Wood:
A Symbolic Analysis of Privacy for TLS 1.3 with Encrypted Client Hello. CCS 2022: 365-379 - [c68]Son Ho, Jonathan Protzenko, Abhishek Bichhawat, Karthikeyan Bhargavan:
Noise*: A Library of Verified High-Performance Secure Channel Protocol Implementations. SP 2022: 107-124 - [i17]Son Ho, Jonathan Protzenko, Abhishek Bichhawat, Karthikeyan Bhargavan:
Noise*: A Library of Verified High-Performance Secure Channel Protocol Implementations (Long Version). IACR Cryptol. ePrint Arch. 2022: 607 (2022) - [i16]Théophile Wallez, Jonathan Protzenko, Benjamin Beurdouche, Karthikeyan Bhargavan:
TreeSync: Authenticated Group Management for Messaging Layer Security. IACR Cryptol. ePrint Arch. 2022: 1732 (2022) - [i15]Richard L. Barnes, Karthikeyan Bhargavan, Benjamin Lipp, Christopher A. Wood:
Hybrid Public Key Encryption. RFC 9180: 1-107 (2022) - 2021
- [c67]Karthikeyan Bhargavan, Abhishek Bichhawat
, Quoc Huy Do, Pedram Hosseyni, Ralf Küsters
, Guido Schmitz
, Tim Würtele
:
A Tutorial-Style Introduction to DY*. Protocols, Strands, and Logic 2021: 77-97 - [c66]Karthikeyan Bhargavan, Abhishek Bichhawat, Quoc Huy Do, Pedram Hosseyni, Ralf Küsters, Guido Schmitz
, Tim Würtele
:
An In-Depth Symbolic Security Analysis of the ACME Standard. CCS 2021: 2601-2617 - [c65]Karthikeyan Bhargavan, Abhishek Bichhawat, Quoc Huy Do, Pedram Hosseyni, Ralf Küsters, Guido Schmitz
, Tim Würtele
:
DY*: A Modular Symbolic Verification Framework for Executable Cryptographic Protocol Code. EuroS&P 2021: 523-542 - [c64]Manuel Barbosa, Gilles Barthe, Karthik Bhargavan, Bruno Blanchet, Cas Cremers, Kevin Liao, Bryan Parno:
SoK: Computer-Aided Cryptography. SP 2021: 777-795 - [i14]Karthikeyan Bhargavan, Abhishek Bichhawat, Quoc Huy Do, Pedram Hosseyni, Ralf Küsters, Guido Schmitz, Tim Würtele:
An In-Depth Symbolic Security Analysis of the ACME Standard. IACR Cryptol. ePrint Arch. 2021: 1457 (2021) - 2020
- [c63]Marina Polubelova, Karthikeyan Bhargavan, Jonathan Protzenko, Benjamin Beurdouche, Aymeric Fromherz, Natalia Kulatova, Santiago Zanella Béguelin:
HACLxN: Verified Generic SIMD Crypto (for all your favourite platforms). CCS 2020: 899-918 - [c62]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
:
EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider. SP 2020: 983-1002 - [e1]Karthikeyan Bhargavan
, Elisabeth Oswald
, Manoj Prabhakaran:
Progress in Cryptology - INDOCRYPT 2020 - 21st International Conference on Cryptology in India, Bangalore, India, December 13-16, 2020, Proceedings. Lecture Notes in Computer Science 12578, Springer 2020, ISBN 978-3-030-65276-0 [contents] - [i13]Marina Polubelova, Karthikeyan Bhargavan, Jonathan Protzenko, Benjamin Beurdouche, Aymeric Fromherz, Natalia Kulatova, Santiago Zanella Béguelin:
HACL×N: Verified Generic SIMD Crypto (for all your favorite platforms). IACR Cryptol. ePrint Arch. 2020: 572 (2020)
2010 – 2019
- 2019
- [j16]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:
Imperfect forward secrecy: how Diffie-Hellman fails in practice. Commun. ACM 62(1): 106-114 (2019) - [c61]Benjamin Lipp
, Bruno Blanchet, Karthikeyan Bhargavan:
A Mechanised Cryptographic Proof of the WireGuard Virtual Private Network Protocol. EuroS&P 2019: 231-246 - [c60]Nadim Kobeissi, Georgio Nicolas, Karthikeyan Bhargavan:
Noise Explorer: Fully Automated Modeling and Verification for Arbitrary Noise Protocols. EuroS&P 2019: 356-370 - [c59]Karthikeyan Bhargavan, Prasad Naldurg:
Practical Formal Methods for Real World Cryptography (Invited Talk). FSTTCS 2019: 1:1-1:12 - [c58]Jonathan Protzenko, Benjamin Beurdouche, Denis Merigoux
, Karthikeyan Bhargavan:
Formally Verified Cryptographic Web Applications in WebAssembly. IEEE Symposium on Security and Privacy 2019: 1256-1274 - [i12]Jonathan Protzenko, Benjamin Beurdouche, Denis Merigoux, Karthikeyan Bhargavan:
Formally Verified Cryptographic Web Applications in WebAssembly. IACR Cryptol. ePrint Arch. 2019: 542 (2019) - [i11]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:
EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider. IACR Cryptol. ePrint Arch. 2019: 757 (2019) - [i10]Manuel Barbosa, Gilles Barthe, Karthikeyan Bhargavan, Bruno Blanchet, Cas Cremers, Kevin Liao, Bryan Parno:
SoK: Computer-Aided Cryptography. IACR Cryptol. ePrint Arch. 2019: 1393 (2019) - 2018
- [c57]Karthikeyan Bhargavan, Franziskus Kiefer, Pierre-Yves Strub:
hacspec: Towards Verifiable Crypto Standards. SSR 2018: 1-20 - [c56]Karthikeyan Bhargavan, Ioana Boureanu, Antoine Delignat-Lavaud, Pierre-Alain Fouque
, Cristina Onete
:
A Formal Treatment of Accountable Proxying Over TLS. IEEE Symposium on Security and Privacy 2018: 799-816 - [i9]Nadim Kobeissi, Karthikeyan Bhargavan:
Noise Explorer: Fully Automated Modeling and Verification for Arbitrary Noise Protocols. IACR Cryptol. ePrint Arch. 2018: 766 (2018) - 2017
- [j15]Benjamin Beurdouche, Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss
, Alfredo Pironti, Pierre-Yves Strub, Jean Karim Zinzindohoue:
A messy state of the union: taming the composite state machines of TLS. Commun. ACM 60(2): 99-107 (2017) - [j14]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:
Verified low-level programming embedded in F. Proc. ACM Program. Lang. 1(ICFP): 17:1-17:29 (2017) - [c55]Jean Karim Zinzindohoué, Karthikeyan Bhargavan, Jonathan Protzenko, Benjamin Beurdouche:
HACL*: A Verified Modern Cryptographic Library. CCS 2017: 1789-1806 - [c54]Karthikeyan Bhargavan, Ioana Boureanu, Pierre-Alain Fouque
, Cristina Onete
, Benjamin Richard:
Content delivery over TLS: a cryptographic analysis of keyless SSL. EuroS&P 2017: 1-6 - [c53]Nadim Kobeissi
, Karthikeyan Bhargavan, Bruno Blanchet
:
Automated Verification for Secure Messaging Protocols and Their Implementations: A Symbolic and Computational Approach. EuroS&P 2017: 435-450 - [c52]Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Nadim Kobeissi:
Formal Modeling and Verification for Domain Validation and ACME. Financial Cryptography 2017: 561-578 - [c51]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:
Everest: Towards a Verified, Drop-in Replacement of HTTPS. SNAPL 2017: 1:1-1:12 - [c50]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:
Implementing and Proving the TLS 1.3 Record Layer. IEEE Symposium on Security and Privacy 2017: 463-482 - [c49]Karthikeyan Bhargavan, Bruno Blanchet, Nadim Kobeissi
:
Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate. IEEE Symposium on Security and Privacy 2017: 483-502 - [i8]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:
Verified Low-Level Programming Embedded in F*. CoRR abs/1703.00053 (2017) - [i7]Jean Karim Zinzindohoué, Karthikeyan Bhargavan, Jonathan Protzenko, Benjamin Beurdouche:
HACL*: A Verified Modern Cryptographic Library. IACR Cryptol. ePrint Arch. 2017: 536 (2017) - 2016
- [j13]Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss
:
miTLS: Verifying Protocol Implementations against Real-World Attacks. IEEE Secur. Priv. 14(6): 18-25 (2016) - [c48]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
:
Formal Verification of Smart Contracts: Short Paper. PLAS@CCS 2016: 91-96 - [c47]Karthikeyan Bhargavan, Gaëtan Leurent
:
On the Practical (In-)Security of 64-bit Block Ciphers: Collision Attacks on HTTP over TLS and OpenVPN. CCS 2016: 456-467 - [c46]Jean Karim Zinzindohoue, Evmorfia-Iro Bartzia, Karthikeyan Bhargavan:
A Verified Extensible Library of Elliptic Curves. CSF 2016: 296-309 - [c45]Karthikeyan Bhargavan, Gaëtan Leurent:
Transcript Collision Attacks: Breaking Authentication in TLS, IKE and SSH. NDSS 2016 - [c44]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
:
Dependent types and multi-monadic effects in F. POPL 2016: 256-270 - [c43]Karthikeyan Bhargavan, Christina Brzuska, Cédric Fournet, Matthew Green, Markulf Kohlweiss
, Santiago Zanella Béguelin
:
Downgrade Resilience in Key-Exchange Protocols. IEEE Symposium on Security and Privacy 2016: 506-525 - [i6]Karthikeyan Bhargavan, Christina Brzuska, Cédric Fournet, Matthew Green, Markulf Kohlweiss, Santiago Zanella Béguelin:
Downgrade Resilience in Key-Exchange Protocols. IACR Cryptol. ePrint Arch. 2016: 72 (2016) - [i5]Karthikeyan Bhargavan, Gaëtan Leurent:
On the Practical (In-)Security of 64-bit Block Ciphers: Collision Attacks on HTTP over TLS and OpenVPN. IACR Cryptol. ePrint Arch. 2016: 798 (2016) - [i4]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:
Implementing and Proving the TLS 1.3 Record Layer. IACR Cryptol. ePrint Arch. 2016: 1178 (2016) - 2015
- [c42]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
:
Imperfect Forward Secrecy: How Diffie-Hellman Fails in Practice. CCS 2015: 5-17 - [c41]Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Alfredo Pironti:
Verified Contributive Channel Bindings for Compound Authentication. NDSS 2015 - [c40]Benjamin Beurdouche, Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss
, Alfredo Pironti, Pierre-Yves Strub, Jean Karim Zinzindohoue:
A Messy State of the Union: Taming the Composite State Machines of TLS. IEEE Symposium on Security and Privacy 2015: 535-552 - [c39]Benjamin Beurdouche, Antoine Delignat-Lavaud, Nadim Kobeissi, Alfredo Pironti, Karthikeyan Bhargavan:
FLEXTLS: A Tool for Testing TLS Implementations. WOOT 2015 - [c38]Antoine Delignat-Lavaud, Karthikeyan Bhargavan:
Network-based Origin Confusion Attacks against HTTPS Virtual Hosting. WWW 2015: 227-237 - [i3]Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Alfredo Pironti, Adam Langley, Marsh Ray:
Transport Layer Security (TLS) Session Hash and Extended Master Secret Extension. RFC 7627: 1-15 (2015) - 2014
- [j12]Chetan Bansal, Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Sergio Maffeis
:
Discovering concrete attacks on website authorization by formal analysis. J. Comput. Secur. 22(4): 601-657 (2014) - [c37]Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss
, Alfredo Pironti, Pierre-Yves Strub, Santiago Zanella Béguelin
:
Proving the TLS Handshake Secure (As It Is). CRYPTO (2) 2014: 235-255 - [c36]Nikhil Swamy, Cédric Fournet, Aseem Rastogi, Karthikeyan Bhargavan, Juan Chen, Pierre-Yves Strub, Gavin M. Bierman:
Gradual typing embedded securely in JavaScript. POPL 2014: 425-438 - [c35]Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Alfredo Pironti, Pierre-Yves Strub:
Triple Handshakes and Cookie Cutters: Breaking and Fixing Authentication over TLS. IEEE Symposium on Security and Privacy 2014: 98-113 - [i2]Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub, Santiago Zanella Béguelin:
Proving the TLS Handshake Secure (as it is). IACR Cryptol. ePrint Arch. 2014: 182 (2014) - 2013
- [j11]Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, Jean Yang:
Secure distributed programming with value-dependent types. J. Funct. Program. 23(4): 402-451 (2013) - [c34]Michael J. May
, Karthikeyan Bhargavan:
Towards Unified Authorization for Android. ESSoS 2013: 42-57 - [c33]Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Sergio Maffeis
:
Defensive JavaScript - Building and Verifying Secure Web Components. FOSAD 2013: 88-123 - [c32]Chetan Bansal, Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Sergio Maffeis
:
Keys to the Cloud: Formal Analysis and Concrete Attacks on Encrypted Web Storage. POST 2013: 126-146 - [c31]Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss
, Alfredo Pironti, Pierre-Yves Strub:
Implementing TLS with Verified Cryptographic Security. IEEE Symposium on Security and Privacy 2013: 445-459 - [c30]Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Sergio Maffeis:
Language-based Defenses Against Untrusted Browser Origins. USENIX Security Symposium 2013: 653-670 - 2012
- [j10]Karthikeyan Bhargavan, Cédric Fournet, Ricardo Corin, Eugen Zalinescu:
Verified Cryptographic Implementations for TLS. ACM Trans. Inf. Syst. Secur. 15(1): 3:1-3:32 (2012) - [c29]Chetan Bansal, Karthikeyan Bhargavan, Sergio Maffeis
:
Discovering Concrete Attacks on Website Authorization by Formal Analysis. CSF 2012: 247-262 - [c28]Karthikeyan Bhargavan, Antoine Delignat-Lavaud:
Web-based Attacks on Host-Proof Encrypted Storage. WOOT 2012: 97-104 - 2011
- [j9]Jesper Bengtson, Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Sergio Maffeis
:
Refinement types for secure implementations. ACM Trans. Program. Lang. Syst. 33(2): 8:1-8:45 (2011) - [c27]Cédric Fournet, Karthikeyan Bhargavan, Andrew D. Gordon:
Cryptographic Verification by Typing for a Sample Protocol Implementation. FOSAD 2011: 66-100 - [c26]Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, Jean Yang:
Secure distributed programming with value-dependent types. ICFP 2011: 266-278 - 2010
- [c25]Karthikeyan Bhargavan, Cédric Fournet, Nataliya Guts:
Typechecking Higher-Order Security Libraries. APLAS 2010: 47-62 - [c24]Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon:
Modular verification of security protocol code by typing. POPL 2010: 445-456
2000 – 2009
- 2009
- [c23]Karthikeyan Bhargavan, Ricardo Corin, Pierre-Malo Deniélou, Cédric Fournet, James J. Leifer:
Cryptographic Protocol Synthesis and Verification for Multiparty Sessions. CSF 2009: 124-140 - [c22]Johannes Borgström, Karthikeyan Bhargavan, Andrew D. Gordon:
A compositional theory for STM Haskell. Haskell 2009: 69-80 - 2008
- [j8]Ricardo Corin, Pierre-Malo Deniélou, Cédric Fournet, Karthikeyan Bhargavan, James J. Leifer:
A secure compiler for session abstractions. J. Comput. Secur. 16(5): 573-636 (2008) - [j7]Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon:
Verifying policy-based web services security. ACM Trans. Program. Lang. Syst. 30(6): 30:1-30:59 (2008) - [j6]Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Stephen Tse:
Verified interoperable implementations of security protocols. ACM Trans. Program. Lang. Syst. 31(1): 5:1-5:61 (2008) - [c21]Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Nikhil Swamy:
Verified implementations of the information card federated identity-management protocol. AsiaCCS 2008: 123-135 - [c20]Karthikeyan Bhargavan, Cédric Fournet, Ricardo Corin, Eugen Zalinescu:
Cryptographically verified implementations for TLS. CCS 2008: 459-468 - [c19]Karthikeyan Bhargavan, Andrew D. Gordon, Iman Narasamdya:
Service Combinators for Farming Virtual Machines. COORDINATION 2008: 33-49 - [c18]Jesper Bengtson, Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Sergio Maffeis
:
Refinement Types for Secure Implementations. CSF 2008: 17-32 - 2007
- [j5]Karthikeyan Bhargavan, Ricardo Corin, Cédric Fournet, Andrew D. Gordon:
Secure sessions for Web services. ACM Trans. Inf. Syst. Secur. 10(2): 8 (2007) - [c17]Ricardo Corin, Pierre-Malo Deniélou, Cédric Fournet, Karthikeyan Bhargavan, James J. Leifer:
Secure Implementations for Typed Session Abstractions. CSF 2007: 170-186 - [c16]Karthikeyan Bhargavan, Andrew D. Gordon, Iman Narasamdya:
Service Combinators for Farming Virtual Machines. TGC 2007: 22 - 2006
- [c15]Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Stephen Tse:
Verified Interoperable Implementations of Security Protocols. CSFW 2006: 139-152 - [c14]Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon:
Verified Reference Implementations of WS-Security Protocols. WS-FM 2006: 88-106 - 2005
- [j4]Karthikeyan Bhargavan, Carl A. Gunter:
Network Event Recognition. Formal Methods Syst. Des. 27(3): 213-251 (2005) - [j3]Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon:
A semantics for web services authentication. Theor. Comput. Sci. 340(1): 102-153 (2005) - [c13]Nishith Krishna, Marc Shapiro, Karthikeyan Bhargavan:
Brief announcement: exploring the consistency problem space. PODC 2005: 168 - [c12]Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Greg O'Shea:
An advisor for web services security policies. SWS 2005: 1-9 - 2004
- [c11]Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon:
Verifying policy-based security for web services. CCS 2004: 268-277 - [c10]Marc Shapiro, Karthikeyan Bhargavan, Nishith Krishna:
A Constraint-Based Formalism for Consistency in Replicated Systems. OPODIS 2004: 331-345 - [c9]Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon:
A semantics for web services authentication. POPL 2004: 198-209 - [c8]Karthikeyan Bhargavan, Ricardo Corin, Cédric Fournet, Andrew D. Gordon:
Secure sessions for web services. SWS 2004: 56-66 - [i1]Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Riccardo Pucella:
TulaFale: A Security Tool for Web Services. CoRR abs/cs/0412044 (2004) - 2003
- [c7]Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Riccardo Pucella:
TulaFale: A Security Tool for Web Services. FMCO 2003: 197-222 - 2002
- [j2]Karthikeyan Bhargavan, Davor Obradovic, Carl A. Gunter:
Formal verification of standards for distance vector routing protocols. J. ACM 49(4): 538-576 (2002) - [j1]Karthikeyan Bhargavan, Carl A. Gunter, Moonjoo Kim, Insup Lee, Davor Obradovic, Oleg Sokolsky, Mahesh Viswanathan:
Verisim: Formal Analysis of Network Simulations. IEEE Trans. Software Eng. 28(2): 129-145 (2002) - [c6]Karthikeyan Bhargavan, Carl A. Gunter:
Requirements for a Practical Network Event Recognition Language. RV@FLoC 2002: 1-20 - 2001
- [c5]Karthikeyan Bhargavan, Satish Chandra, Peter J. McCann, Carl A. Gunter:
What packets may come: automata for network monitoring. POPL 2001: 206-219 - 2000
- [c4]Karthikeyan Bhargavan, Carl A. Gunter, Davor Obradovic:
Fault origin adjudication. FMSP 2000: 61-71 - [c3]Karthikeyan Bhargavan, Carl A. Gunter, Moonjoo Kim, Insup Lee, Davor Obradovic, Oleg Sokolsky, Mahesh Viswanathan:
Verisim: Formal analysis of network simulations. ISSTA 2000: 2-13 - [c2]Karthikeyan Bhargavan, Carl A. Gunter, Davor Obradovic:
Routing Information Protocol in HOL/SPIN. TPHOLs 2000: 53-72
1990 – 1999
- 1998
- [c1]Karthikeyan Bhargavan, Carl A. Gunter, Elsa L. Gunter, Michael Jackson, Davor Obradovic, Pamela Zave:
The Village Telephone System: A Case Study in Formal Software Enginee