![](https://dblp.dagstuhl.de/img/logo.ua.320x120.png)
![](https://dblp.dagstuhl.de/img/dropdown.dark.16x16.png)
![](https://dblp.dagstuhl.de/img/peace.dark.16x16.png)
Остановите войну!
for scientists:
![search dblp search dblp](https://dblp.dagstuhl.de/img/search.dark.16x16.png)
![search dblp](https://dblp.dagstuhl.de/img/search.dark.16x16.png)
default search action
Karthikeyan Bhargavan
Person information
- affiliation: INRIA, France
Refine list
![note](https://dblp.dagstuhl.de/img/note-mark.dark.12x12.png)
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
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 Engineering. TPHOLs 1998: 49-66
Coauthor Index
![](https://dblp.dagstuhl.de/img/cog.dark.24x24.png)
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-08-03 20:11 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint