Publications (list)

 

Theses

  1. 1.Network Event Recognition, K. Bhargavan. Ph.D. Dissertation, University of Pennsylvania, 2003.

  2. 2.Automated Proof Support for Reasoning about Mobile Distributed Programs, K. Bhargavan. Undergraduate Thesis, Indian Institute of Technology Delhi, 1997.


Refereed Journals

  1. 1.Verified Cryptographic Implementations for TLS,K. Bhargavan, C. Fournet, R. Corin, and E. Zalinescu. ACM Transactions on Information and System Security, 15(1), 2012.

  2. 2.Refinement Types for Secure Implementations, J. Bengtson, K. Bhargavan, C. Fournet, A.D. Gordon, and S. Maffeis. ACM Transactions on Programming Languages and Systems, 33(2), 2011.

  3. 3.Verified interoperable implementations of security protocols, K. Bhargavan, C. Fournet, A.D. Gordon, and S. Tse. ACM Transactions on Programming Languages and Systems, 31(1):5, 2008.

  4. 4.Verifying policy-based web services security, K. Bhargavan, C. Fournet, and A.D. Gordon. ACM Transactions on Programming Languages and Systems, 30(6):30, 2008.

  5. 5.A secure compiler for session abstractions, R. Corin, P-M. Deniélou, C. Fournet, K. Bhargavan, and J.J. Leifer. Journal of Computer Security 16(5): 573–636, 2008.

  6. 6.Secure sessions for Web services, K. Bhargavan, R. Corin, C. Fournet, and A.D. Gordon. ACM Transactions on Information and System Security, 10(2):8, 2007.

  7. 7.A semantics for web services authentication, K. Bhargavan, C. Fournet, and A.D. Gordon. Theoretical Computer Science, 340(1), 102–153, 2005.

  8. 8.Network Event Recognition, K. Bhargavan and C.A. Gunter. Formal Methods in System Design, 27(3): 213–251, 2005.

  9. 9.Verisim: Formal Analysis of Network Simulations, K. Bhargavan, C.A. Gunter, M. Kim, I. Lee, D. Obradovic, O. Sokolsky, M. Viswanathan. IEEE Transactions on Software Engineering, 28(2): 129–145, 2002.

  10. 10.Formal verification of standards for distance vector routing protocols, K. Bhargavan, D. Obradovic, and C.A. Gunter. Journal of the ACM, 49(4): 538–576, 2002.


Refereed Conferences

  1. 1.Discovering Concrete Attacks on Website Authorization by Formal Analysis, C. Bansal, K. Bhargavan, and S. Maffeis. 25th IEEE Computer Security Foundations Symposium (CSF 2012), 2012, to appear.

  2. 2.Secure Distributed Programming with Value-dependent Types, N. Swamy, J. Chen, C. Fournet, P-Y. Strub, K. Bhargavan, and J. Yang. 16th ACM SIGPLAN International Conference on Functional Programming (ICFP 2011), 266-278, 2011.

  3. 3.Typechecking Higher-Order Security Libraries, K. Bhargavan, C. Fournet, and N. Guts. Asian Symposium on Programming Languages and Systems (APLAS), 47-62, 2010.

  4. 4.Modular Verification of Security Protocol Code by Typing, K. Bhargavan, C. Fournet, A.D. Gordon. ACM Symposium on Principles of Programming Languages, 445-456, 2010.

  5. 5.Secure Distributed Programming with Value-dependent Types, N. Swamy, J. Chen, C. Fournet, P-Y. Strub, K. Bhargavan, and J. Yang. 16th ACM SIGPLAN International Conference on Functional Programming (ICFP 2011), 266-278, 2011.

  6. 6.Typechecking Higher-Order Security Libraries, K. Bhargavan, C. Fournet, and N. Guts. Asian Symposium on Programming Languages and Systems (APLAS), 47-62, 2010.

  7. 7.Modular Verification of Security Protocol Code by Typing, K. Bhargavan, C. Fournet, A.D. Gordon. ACM Symposium on Principles of Programming Languages, 445-456, 2010.

  8. 8.A Compositional Theory of STM Haskell, J. Borgström, K. Bhargavan, and A.D. Gordon. ACM Symposium on Haskell, 69–80, 2009.

  9. 9.Cryptographic Protocol Synthesis and Verification for Multiparty Sessions, K. Bhargavan, R. Corin, P-M. Deniélou, C. Fournet, and J.J. Leifer. IEEE Computer Security Foundations, 124–140, 2009.

  10. 10.Cryptographically verified implementations for TLS, K. Bhargavan, R. Corin, C. Fournet, and E. Zalinescu. ACM Conference on Computer and Communications Security, 459–468, 2008.

  11. 11.Verified implementations of the information card federated identity-management protocol, K. Bhargavan, C. Fournet, A.D. Gordon, and N. Swamy. ACM Symposium on InformAtion, Computer and Communications Security, 123–135, 2008.

  12. 12.Service Combinators for Farming Virtual Machines, K. Bhargavan, A.D. Gordon, and I. Narasamdya. International Conference on Coordination Models and Languages, 33–49, 2008.

  13. 13.Refinement Types for Secure Implementations, J. Bengtson, K. Bhargavan, C. Fournet, A.D. Gordon, and S. Maffeis. IEEE Computer Security Foundations Symposium, 17–32, 2008.

  14. 14.Secure Implementations for Typed Session Abstractions, R. Corin, P-M. Deniélou, C. Fournet, K. Bhargavan, and J.J. Leifer. IEEE Computer Security Foundations Symposium, 170–186, 2007.

  15. 15.Verified Interoperable Implementations of Security Protocols, K. Bhargavan, C. Fournet, A.D. Gordon, and S. Tse. IEEE Computer Security Foundations Workshop, 139–152, 2006.

  16. 16.Verifying policy-based security for web services, K. Bhargavan, C. Fournet, and A.D. Gordon. ACM Conference on Computer and Communications Security, 268–277, 2004.

  17. 17.Constraint-Based Formalism for Consistency in Replicated Systems, K. Bhargavan, M. Shapiro, and N. Krishna. International Conference on Principles of Distributed Systems, 331–345, 2004.

  18. 18.A semantics for web services authentication, K. Bhargavan, C. Fournet, and A.D. Gordon. ACM Symposium on Principles of Programming Languages, 198–209, 2004.

  19. 19.TulaFale: A Security Tool for Web Services, K. Bhargavan, C. Fournet, A.D. Gordon, and R. Pucella. International Symposium on Formal Methods for Components and Objects, 197–222, 2003.

  20. 20.What packets may come: automata for network monitoring, K. Bhargavan, S. Chandra, P.J. McCann, and C.A. Gunter. ACM Symposium on Principles of Programming Languages, 206–219, 2001.

  21. 21.Verisim: Formal analysis of network simulations, K. Bhargavan, C.A. Gunter, M. Kim, I. Lee, D. Obradovic, O. Sokolsky, M. Viswanathan. ACM International Symposium on Software Testing and Analysis, 2–13, 2000.

  22. 22.Routing Information Protocol in HOL/SPIN, K. Bhargavan, C.A. Gunter and D. Obradovic. International Conference on Theorem Proving in Higher Order Logics, 53–72, 2000.

  23. 23.The Village Telephone System: A Case Study in Formal Software Engineering, K. Bhargavan, C.A. Gunter, E.L. Gunter, M. Jackson, D. Obradovic, and P. Zave. International Conference on Theorem Proving in Higher Order Logics, 49–66, 1998.


Refereed Workshops

  1. 1.Pre- and Post-conditions for Security Typechecking, K. Bhargavan, C. Fournet, and N. Guts. Workshop on Foundations of Security and Privacy (FSC-PrivMod), 2010.

  2. 2.Verified Reference Implementations of WS-Security Protocols, K. Bhargavan, C. Fournet, and A.D. Gordon. International Workshop on Web Services and Formal Methods, 88–106, 2006.

  3. 3.An advisor for web services security policies, K. Bhargavan, C. Fournet, A.D. Gordon, G. O’Shea. ACM Workshop on Secure Web Services, 1–9, 2005.

  4. 4.Secure sessions for web services, K. Bhargavan, R. Corin, C. Fournet, and A.D. Gordon. ACM Workshop on Secure Web Services, 56–66, 2004.

  5. 5.Requirements for a Practical Network Event Recognition Language, K. Bhargavan and C.A. Gunter. Workshop on Runtime Verification, ENTCS 70(4), 2002.

  6. 6.Fault origin adjudication, K. Bhargavan, C.A. Gunter, and D. Obradovic. Workshop on Formal Methods in Software Practice, 61–71, 2000.


Technical Reports and Short Papers

  1. 1.Refinement Types for Secure Implementations, J. Bengtson, K. Bhargavan, C. Fournet, A.D. Gordon, and S. Maffeis. Technical Report MSR-TR-2008-118, Microsoft Research, 2008.

  2. 2.Cryptographically Verified Implementations for TLS, K. Bhargavan, R. Corin, C. Fournet, and E. Zalinescu. Workshop on Formal and Computational Cryptography, 2008.

  3. 3.The Rise and Rise of the Declarative Datacentre, K. Bhargavan, A.D. Gordon, T. Harris, and P. Toft, editors. Microsoft Research Technical Report TR-2008-61, 2008.

  4. 4.Getting operations logic right: types, service-orientation, and static analysis, K. Bhargavan and A.D. Gordon. Workshop on the The Rise and Rise of the Declarative Datacentre, 2008.

  5. 5.Service Combinators for Farming Virtual Machines, K. Bhargavan, A.D. Gordon, and I. Narasamdya. Technical Report MSR-TR-2007-165, Microsoft Research, 2007.

  6. 6.Crypto-Verifying Protocol Implementations in ML, K. Bhargavan, R. Corin, and C. Fournet. Workshop on Formal and Computational Cryptography, 2007.

  7. 7.Verified Interoperable Implementations of Security Protocols, K. Bhargavan, C. Fournet, A.D. Gordon, and S. Tse. Technical Report MSR-TR-2006-46, Microsoft Research, 2006.

  8. 8.Brief announcement: exploring the consistency problem space, N. Krishna, M. Shapiro, and K. Bhargavan. ACM Symposium on Principles of Distributed Computing, 168, 2005.

  9. 9.Verifying policy-based web services security, K. Bhargavan, C. Fournet, and A.D. Gordon. Technical Report MSR-TR-2004-84, Microsoft Research, 2004.

  10. 10.A formalism for consistency and partial replication, K. Bhargavan, M. Shapiro, Y. Chong, and Y. Hamadi. Technical Report MSR-TR-2004-58, Microsoft Research, 2004.

  11. 11.The Actions-Constraints approach to replication: Definitions and proofs, K. Bhargavan and M. Shapiro. Technical Report MSR-TR-2004-14, Microsoft Research, 2004.

  12. 12.A semantics for web services authentication, K. Bhargavan, C. Fournet, and A.D. Gordon. Technical Report MSR-TR-2003-83, Microsoft Research, 2004.

  13. 13.Mechanizing various pi-calculi in HOL, B. Karthikeyan, S. Prasad, and T.R. Vishwanath. Supplementary Proceedings, International Conference on Theorem Proving in Higher Order Logics, 1997.