My research concerns the theory, design, and implementation of modern programming language features and formal verification techniques. My recent work focuses on using formal methods to investigate the (in)security of distributed applications such as cryptographic protocols.

Publications: A complete list of my publications with download links can be found over on this page. A version with more details is on this other page.

Projects: CRYSP, Cryptographic Verification Kit, Refinement Types for F#, Secure Multi-party Sessions, Web Services Security

Grants: ERC Starting Grant 2010: CRYSP: Collaborative Cryptographic Security Proofs for Programs

Software: F*, F7, FS2PV, FS2CV, S2ML, TulaFale

News:

1. •[Paper] Discovering Concrete Attacks on Website Authorization by Formal Analysis, C Bansal, K Bhargavan, S Maffeis, CSF, June 2012, to appear
   

2. •[Paper] Verified Cryptographic Implementations for TLS, K Bhargavan, C Fournet, R Corin, E Zalinescu, TISSEC, March 2012
   

3. •[Project] PROSECCO is now an INRIA équipe-projet.
   

4. •[Offers] Summer and masters' internships (stages) 2012: Topics [1,2,3].
   To apply, email me with your CV.
   

5. •[Offers] Ph.D studentships, and post-docs available in the PROSECCO project, funded by the ERC Grant CRYSP. To apply, email me with your CV and references.