Publications

The papers given here are not necessarily identical to any previously published paper. Copyright and all rights therein are maintained by the authors or by other copyright holders. Additional bibliographic details appear in these bibtex and pdf files. Please contact me if you don't find the paper you are looking for.


Conference papers

Self-Certification: Bootstrapping Certified Typecheckers in F* with Coq (.pdf), with Pierre-Yves Strub, Nikhil Swamy, and Juan Chen, in ACM Symposium on Principles of Programming Languages (POPL'12), pages 571--583. January 2012. © ACM.

Information-Flow Types for Homomorphic Encryptions (.pdf), with Jérémy Planul and Tamara Rezk, in 18th ACM Conference on Computer and Communications Security (CCS'11), pages 351--360. October 2011. © ACM.

Modular Code-Based Cryptographic Verification (.pdf), with Markulf Kohlweiss and Pierre-Yves Strub, in 18th ACM Conference on Computer and Communications Security (CCS'11), pages 341--350. October 2011. © ACM.

Secure Distributed Programming with Value-Dependent Types (.pdf), with Nikhil Swamy, Juan Chen, Pierre-Yves Strub, Karthikeyan Bhargavan, and Jean Yang, in ICFP. September 2011. See also the full paper at MSR-TR-2011-37.

Compiling Information-Flow Security to Minimal Trusted Computing Bases (.pdf), with Jérémy Planul, in Programming Languages and Systems (ESOP'11), LNCS 6602, pages 216--235. March 2011. © Springer-Verlag.

Typechecking Higher-Order Security Libraries, with Karthikeyan Bhargavan and Nataliya Guts, in APLAS, pages 47--62. 2010.

Modular Verification of Security Protocol Code by Typing (.pdf), with K. Bhargavan and A. D. Gordon, in ACM Symposium on Principles of Programming Languages (POPL'10), pages 445--456. January 2010. © ACM.

A Security-Preserving Compiler for Distributed Programs: From Information-Flow Policies to Cryptographic Mechanisms (.pdf), with Gurvan le Guernic and Tamara Rezk, in ACM Conference on Computer and Communications Security (CCS'09), pages 432--441. November 2009. © ACM.

Reliable Evidence: Auditability by Typing (.pdf), with Nataliya Guts and Francesco Zappa Nardelli, in 14th European Symposium on Research in Computer Security (ESORICS 2009), LNCS 5789, pages 168--183. September 2009. © Springer-Verlag.

Secure Enforcement for Global Process Specifications (.pdf), with Jérémy Planul and Ricardo Corin, in 20th International Conference on Concurrency Theory (CONCUR'09), LNCS 5710, pages 511--526. September 2009. © Springer-Verlag.

Cryptographic Protocol Synthesis and Verification for Multiparty Sessions (.pdf), with Karthikeyan Bhargavan, Ricardo Corin, Pierre-Malo Deniélou, and James J. Leifer, in 22nd IEEE Computer Security Foundations Symposium (CSF'09), pages 124--140. July 2009. © IEEE.

High-Level Programming for E-Cash (Extended Abstract), with Nataliya Guts and Francesco Zappa Nardelli, in 1st Computational and Symbolic Proofs of Security Workshop. 2009.

Cryptographically Verified Implementations for TLS (.pdf), with Karthikeyan Bhargavan, Ricardo Corin, and Eugen Zalinescu, in ACM Conference on Computer and Communications Security (CCS'08), pages 459--468. October 2008. © ACM.

Code-Carrying Authorization (.pdf), with Sergio Maffeis, Martín Abadi, and Andrew D. Gordon, in 13th European Symposium on Research in Computer Security (ESORICS'08), LNCS 5283, pages 563-579. October 2008. © Springer-Verlag.

Refinement Types for Secure Implementations (.pdf), with Jesper Bengtson, Karthikeyan Bhargavan, Andrew D. Gordon, and Sergio Maffeis, in 21st IEEE Computer Security Foundations Symposium (CSF'08), pages 17--32. June 2008. © IEEE.

A Formal Implementation of Value Commitment (.pdf), with Nataliya Guts and Francesco Zappa Nardelli, in Programming Languages and Systems (ESOP'08), LNCS 4960, pages 383--397. March 2008. © Springer-Verlag.

Verified Implementations of the Information Card Federated Identity-Management Protocol (.pdf), with Karthikeyan Bhargavan, Andrew D. Gordon, and Nikhil Swamy, in Proceedings of the ACM Symposium on Information, Computer and Communications Security (ASIACCS'08), pages 123--135. March 2008. © ACM.

Cryptographically Sound Implementations for Typed Information-Flow Security (.pdf), with Tamara Rezk, in 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'08), pages 323--335. January 2008. © ACM.

Secure Implementations of Typed Session Abstractions (.pdf), with Ricardo Corin, Pierre-Malo Deniélou, Karthikeyan Bhargavan, and James J. Leifer, in 20th IEEE Computer Security Foundations Symposium (CSF20), pages 170--186. July 2007. © IEEE.

Design and Semantics of a Decentralized Authorization Language (.pdf), with Moritz Y. Becker and Andrew D. Gordon, in 20th IEEE Computer Security Foundations Symposium (CSF20), pages 3--15. July 2007. © IEEE.

A Type Discipline for Authorization in Distributed Systems (.pdf), with Andrew D. Gordon and Sergio Maffeis, in 20th IEEE Computer Security Foundations Symposium (CSF20), pages 31--45. July 2007. © IEEE.

Computational Secrecy by Typing for the Pi Calculus (.pdf), with Martín Abadi and Ricardo Corin, in Programming Languages and Systems 4th Asian Symposium (APLAS 2006), LNCS 4279, pages 253--269. November 2006. © Springer-Verlag.

Verified Reference Implementations of WS-Security Protocols (.pdf), with Karthikeyan Bhargavan and Andrew D. Gordon, in Web Services and Formal Methods, Third International Workshop (WS-FM 2006), LNCS 4184, pages 88--106. September 2006. © Springer-Verlag.

Cryptographically Sound Implementations for Communicating Processes (Extended Abstract) (.pdf), with Pedro Adao, in 33rd International Colloquium on Automata, Languages and Programming (ICALP 2006), LNCS 4052, pages 83--94. July 9--16 2006. © Springer-Verlag.

Verified Interoperable Implementations of Security Protocols (.pdf), with Karthikeyan Bhargavan, Andrew D. Gordon, and Stephen Tse, in 19th IEEE Computer Security Foundations Workshop (CSFW'06), pages 139--152. June 2006. © IEEE.

An Advisor for Web Services Security Policies (.pdf), with Karthikeyan Bhargavan, Andrew D. Gordon, and Greg O'Shea, in SWS'05: Proceedings of the 2005 ACM Workshop on Secure Web Service, pages 1--9. October 2005. © ACM.

Automated Verification of Selected Equivalences for Security Protocols (.pdf), with Bruno Blanchet and Martín Abadi, in 20th IEEE Symposium on Logic in Computer Science (LICS 2005), pages 331--340. June 2005. The full version now appears in Journal of Logic and Algebraic Programming. © IEEE.

A Type Discipline for Authorization Policies (.pdf), with Andrew D. Gordon and Sergio Maffeis, in Programming Languages and Systems, 14th European Symposium on Programming, ESOP 2005, LNCS 3444, pages 141--156. April 2005. © Springer-Verlag.

Secure Sessions for Web Services (.pdf), with Karthikeyan Bhargavan, Ricardo Corin, and Andrew D. Gordon, in SWS'04: Proceedings of the 2004 Workshop on Secure Web Services, pages 56--66. October 2004. © ACM.

Verifying Policy-Based Security for Web Services (.pdf), with K. Bhargavan and A. D. Gordon, in 11th ACM Conference on Computer and Communications Security (CCS'04), pages 268-277. October 2004. © ACM.

Ethernet Topology Discovery without Network Assistance (.pdf), with Richard Black and Austin Donnelly, in Proceedings of the 12th IEEE International Conference on Network Protocols (ICNP 2004), pages 328--339. October 2004. © IEEE.

Stuck-Free Conformance (.ps), with C. A. R. Hoare, Sriram K. Rajamani, and Jakob Rehof, in Proceedings of the 16th International Conference on Computer Aided Verification (CAV'04), LNCS 3114, pages 242--254. July 2004. © Springer-Verlag.

TulaFale: A Security Tool for Web Services (.pdf), with K. Bhargavan, A. D. Gordon, and R. Pucella, in International Symposium on Formal Methods for Components and Objects (FMCO'03), LNCS 3188, pages 197--222. 2004. © Springer-Verlag.

From Stack Inspection to Access Control: A Security Analysis for Libraries (.ps), with Frédéric Besson, Tomasz Blanc, and Andrew D. Gordon, in 17th IEEE Computer Security Foundations Workshop (CSFW'04), pages 61--75. June 2004. © IEEE.

Just Fast Keying in the Pi Calculus (.pdf), with Martín Abadi and Bruno Blanchet, in Programming Languages and Systems, 13th European Symposium on Programming, ESOP 2004, LNCS 2986, pages 340--354. March 2004. © Springer-Verlag.

A Semantics for Web Services Authentication (.pdf), with K. Bhargavan and A. D. Gordon, in 31st ACM Symposium on Principles of Programming Languages (POPL'04), pages 198--209. January 2004. An extended version appears as Microsoft Research Technical Report MSR-TR-2003-83. © ACM.

Access Control based on Execution History (.pdf) (.ps), with Martín Abadi, in Network and Distributed System Security Symposium (NDSS'03), pages 107--121. February 2003. © Internet Society.

Hiding Names: Private Authentication in the Applied Pi Calculus (.pdf) (.ps), with Martín Abadi, in Software Security -- Theories and Systems. Mext-NSF-JSPS International Symposium, Tokyo, November 2002 (ISSS'02), LNCS 2609, pages 317--338. 2003. © Springer-Verlag.

Stack Inspection: Theory and Variants (.pdf) (.ps), with Andrew D. Gordon, in Conference record of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'02), pages 307--318. January 2002. © ACM.

Modern Concurrency Abstractions for C# (.pdf) (.ps), with Nick Benton and Luca Cardelli, in ECOOP 2002 -- Object Oriented Programming, LNCS 2374, pages 415--440. June 2002. © Springer-Verlag.

Mobile values, new names, and secure communication (.pdf) (.ps), with Martín Abadi, in 28th ACM Symposium on Principles of Programming Languages (POPL'01), pages 104--115. 2001. © ACM.

Authentication Primitives and their Compilation (.pdf) (.ps), with Martín Abadi and Georges Gonthier, in Conference record of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'00), pages 302--315. January 2000. © ACM.

An Asynchronous, Distributed Implementation of Mobile Ambients (.pdf) (.ps), with Jean-Jacques Lévy and Alan Schmitt, in Proceedings of IFIP TCS 2000, LNCS 1872, pages 348--364. 17--19 August 2000. © Springer-Verlag.

Inheritance in the join-calculus (Extended Abstract) (.pdf) (.ps), with Cosimo Laneve, Luc Maranget, and Didier Rémy, in FST TCS 2000: Foundations of Software Technology and Theoretical Computer Science, LNCS 1974, pages 397--408. December 2000. The full version now appears in Journal of Logic and Algebraic Programming. © Springer-Verlag.

A Top-Down Look at a Secure Message (.ps), with Martín Abadi and Georges Gonthier, in Proceedings of the Nineteenth Conference on the Foundations of Software Technology and Theoretical Computer Science (FST&TCS '99), LNCS 1738, pages 122--141. December 1999. © Springer-Verlag.

Secure Communications Processing for Distributed Languages (.pdf) (.ps), with Martín Abadi and Georges Gonthier, in Proceedings of the 1999 IEEE Symposium on Security and Privacy, pages 74--88. May 1999. © IEEE.

An Implementation of Ambients in JoCaml, with Alan Schmitt, in 5th Mobile Object Systems Workshop: Programming Languages for Wide-Area Networks. June 1999.

Secure Implementation of Channel Abstractions (.ps), with Martín Abadi and Georges Gonthier, in Proceedings of LICS '98, pages 105--116. June 1998. © IEEE.

Bisimulations in the Join-Calculus (.ps), with Michele Boreale and Cosimo Laneve, in Programming Concepts and Methods, IFIP TC2/WG2.2,2.3 International Conference on Programming Concepts and Methods (PROCOMET '98). June 1998. © Chapman and Hall.

A Hierarchy of Equivalences for Asynchronous Calculi (extended abstract) (.ps), with Georges Gonthier, in Proceedings of the 25th International Colloquium on Automata, Languages and Programming (ICALP '98), LNCS 1443, pages 844-855. July 1998. © Springer-Verlag.

Implicit Typing à la ML for the join-calculus (.ps), with Cosimo Laneve, Luc Maranget, and Didier Rémy, in Proceedings of the 8th International Conference on Concurrency Theory (CONCUR'97), LNCS 1243, pages 196--212. 1--4 July 1997. © Springer-Verlag.

A Calculus of Mobile Agents (.ps), with Georges Gonthier, Jean-Jacques Lévy, Luc Maranget, and Didier Rémy, in Proceedings of the 7th International Conference on Concurrency Theory (CONCUR '96), LNCS 1119, pages 406--421. 26--29 August 1996. © Springer-Verlag.

The Reflexive Chemical Abstract Machine and the Join-Calculus (.ps), with Georges Gonthier, in Conference record of the 23th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'96), pages 372--385. January 1996. © ACM.


Lecture notes

Cryptographic Verification by Typing for a Sample Protocol Implementation (.pdf), with Karthik Bhargavan and Andrew D. Gordon, in Proceedings of the Foundations of Seccurity and Design VI Summer School (FOSAD 2010), LNCS. September 2011. © IOS Press. © Springer-Verlag.

Principles and Applications of Refinement Types, with Andrew D. Gordon, in International Summer School Logics and Languages for Reliability and Security, Marktoberdorf, August 2009. October 2010. Also Technical Report MSR-TR-2009-147. © IOS Press.

JoCaml: a Language for Concurrent Distributed and Mobile Programming (.pdf), with Fabrice Le Fessant, Luc Maranget, and Alan Schmitt, in Advanced Functional Programming, 4th International School, Oxford, August 2002, LNCS 2638, pages 129--158. 2003. © Springer-Verlag.

The Join Calculus: a Language for Distributed Mobile Programming (.pdf) (.ps), with Georges Gonthier, in Applied Semantics. International Summer School, APPSEM 2000, Caminha, Portugal, September 2000, LNCS 2395, pages 268--332. August 2002. © Springer-Verlag.


Articles in Journals

Refinement Types for Secure Implementations, with Jesper Bengtson, Karthikeyan Bhargavan, Andrew D. Gordon, and Sergio Maffeis, ACM Transactions on Programming Languages and Systems. 2010. To appear. An short version appears in CSF'08. See also Microsoft Research Technical Report MSR-TR-2008-118 SP1. © ACM.

SecPAL: Design and Semantics of a Decentralized Authorization Language, with Moritz Y. Becker and Andrew D. Gordon, Journal of Computer Security (Special issue for CSF'07). 2009. To appear. © IOS Press.

A Secure Compiler for Session Abstractions, with Ricardo Corin, Pierre-Malo Deniélou, Karthikeyan Bhargavan, and James J. Leifer, Journal of Computer Security (Special issue for CSF'07) 16(5):573--636. 2008. © IOS Press.

Automated Verification of Selected Equivalences for Security Protocols (.pdf), with Bruno Blanchet and Martín Abadi, Journal of Logic and Algebraic Programming 75(1):3--51. 2008. A short version appears in LICS'05. © Elsevier.

Verified Interoperable Implementations of Security Protocols, with Karthikeyan Bhargavan, Andrew D. Gordon, and Stephen Tse, ACM Transactions on Programming Languages and Systems 31(1):1--61. December 2008. © ACM.

Verifying Policy-Based Web Services Security, with Karthikeyan Bhargavan and Andrew D. Gordon, ACM Transactions on Programming Languages and Systems 30(6). October 2008. © ACM.

Just Fast Keying in the Pi Calculus, with Martín Abadi and Bruno Blanchet, ACM Transactions on Information and System Security (TISSEC) 10(3). July 2007. An extended abstract appears in Programming Languages and Systems, 13th European Symposium on Programming, ESOP 2004. © ACM.

A Type Discipline for Authorization Policies, with A. D. Gordon and S. Maffeis, ACM Transactions on Programming Languages and Systems 29(5). August 2007. © ACM.

Secure Sessions for Web Services (.pdf), with Karthikeyan Bhargavan, Ricardo Corin, and Andrew D. Gordon, ACM Transactions on Information and System Security (TISSEC) 10(2). May 2007. © ACM.

A Hierarchy of Equivalences for Asynchronous Calculi (.pdf) (.ps), with Georges Gonthier, Journal of Logic and Algebraic Programming 63(1):131--173. April 2005. An extended abstract appears in ICALP'98. © Elsevier.

A Semantics for Web Services Authentication, with Karthikeyan Bhargavan and Andrew D. Gordon, Theoretical Computer Science 340(1):102--153. June 2005. See also Microsoft Research Technical Report MSR-TR-2003-83. © Elsevier.

Private Authentication (.pdf), with Martín Abadi, Theoretical Computer Science 322(3):427--476. September 2004. Special issue on Foundations of Wide Area Network Computing. Parts of this work were presented at PET'02 (LNCS 2482) and ISSS'02 (LNCS 2602). © Elsevier.

Modern Concurrency Abstractions for C# (.pdf), with Nick Benton and Luca Cardelli, ACM Transactions on Programming Languages and Systems 26(5):769--804. September 2004. An extended abstract appears in ECOOP'02 (LNCS 2374). © ACM.

Stack Inspection: Theory and Variants (.pdf), with Andrew D. Gordon, ACM Transactions on Programming Languages and Systems 25(3):360--399. 2003. An extended abstract appears in POPL'02. © ACM.

Inheritance in the join calculus, with Cosimo Laneve, Luc Maranget, and Didier Rémy, Journal of Logic and Algebraic Programming 57(1--2):23--69. September 2003. © Elsevier.

Secure Implementation of Channel Abstractions, with Martín Abadi and Georges Gonthier, Information and Computation 174(1):37--83. April 2002. © Elsevier.

Bisimulations in the Join-Calculus (.pdf) (.ps), with Cosimo Laneve, Theoretical Computer Science 266(1-2):569--603. September 2001. © Elsevier.


Others

Pre- and Post-Conditions for Security Typechecking (.pdf), with Karthikeyan Bhargavan and Nataliya Guts, in Workshop on Foundations of Security and Privacy (FCS-PrivMod 2010). July 2010.

Refinement Types for Secure Implementations (.pdf), with Jesper Bengtson, Karthikeyan Bhargavan, Andrew D. Gordon, and Sergio Maffeis, Microsoft Research Technical Report (MSR-TR-2008-118). 2008. Revised: 2010.

Trustworthy Global Computing, Third Symposium, TGC 2007, Sophia-Antipolis, France, November 5-6, 2007, Revised Selected Papers, with Gilles Barthe, LNCS 4912. 2008. © Springer-Verlag.

A Secure Compiler for Session Abstractions, with Ricardo Corin, Pierre-Malo Deniélou, Karthikeyan Bhargavan, and James Leifer, MSR-INRIA Joint Centre . 2008. Prototype implementation available at \urlhttp://msr-inria.inria.fr/projects/sec/sessions.

A Computational Verifier for Protocol Code (fs2cv), with Karthikeyan Bhargavan, Ricardo Corin, and Eugen Zalinescu, MSR-INRIA Joint Centre . 2008. Prototype implementation available at \urlhttp://msr-inria.inria.fr/projects/sec/fs2cv.

Crypto-Verifying Protocol Implementations in ML, with Karthikeyan Bhargavan and Ricardo Corin, in Proceedings of the 3rd Workshop on Formal and Computational Cryptography (FCC'07). July 2007.

SecPAL: Design and Semantics of a Decentralized Authorization Language (.pdf), with Moritz Y. Becker and Andrew D. Gordon, Microsoft Research Technical Report (MSR-TR-2006-120). September 2006.

A Type Discipline for Authorization Policies, with A. D. Gordon and S. Maffeis, Microsoft Research (MSR-TR-2005-01). 2005.

Stuck-Free Conformance (.ps), with C. A. R. Hoare, Sriram K. Rajamani, and Jakob Rehof, Microsoft Research Technical Report (MSR-TR-2004-69). July 2004.

A Semantics for Web Services Authentication (.pdf), with Karthikeyan Bhargavan and Andrew D. Gordon, Microsoft Research Technical Report (MSR-TR-2003-83). February 2004.

Secure Sessions for Web Services, with Karthikeyan Bhargavan, Ricardo Corin, and Andrew D. Gordon, Microsoft Research Technical Report (MSR-TR-2004-114). 2004.

A Distributed Implementation of Ambients (.ps), with Jean-Jacques Lévy and Alan Schmitt. 2000. Manuscript, subsumes papers presented at MOS'99 and FST-TCS 2000.

Secure implementation of channel abstractions (.ps), with Martín Abadi and Georges Gonthier. September 2000. Manuscript, subsumes papers presented at LICS'98 and S&P'99.

Weak Bisimulations by Decreasing Diagrams, with Georges Gonthier. March 1999. Draft.

An Implementation of Ambients in JoCAML, with Alan Schmitt. 1999. Software available from http://join.inria.fr/ambients.html.

The Join-Calculus language (version 1.03), with Luc Maranget. June 1997. Source distribution and documentation available from http://join.inria.fr/.


Dissertation

The Join-Calculus: a Calculus for Distributed Mobile Programming (.ps.gz) (.pdf). November 1998. Ecole Polytechnique, Palaiseau. Also published by INRIA, TU-0556.


Revised: 06-03-2012.