Cédric Fournet

147 papers A* 42A 17B 8Misc 1Journal 50Unranked 27

Year	Rank	Type	Title / Venue / Authors
2025	J	`jnl`	Enter, Exit, Page Fault, Leak: Testing Isolation Boundaries for Microarchitectural Leaks. CoRR Oleksii Oleksenko, Flavien Solt, Cédric Fournet, Jana Hofmann, Boris Köpf, Stavros Volos
2025	A*	`conf`	Transparent Attested DNS for Confidential Computing Services. USENIX Security Symposium Antoine Delignat-Lavaud, Cédric Fournet, Kapil Vaswani, Manuel Costa, Sylvan Clebsch, Christoph M. Wintersteiger
2025	J	`jnl`	Transparent Attested DNS for Confidential Computing Services. CoRR Antoine Delignat-Lavaud, Cédric Fournet, Kapil Vaswani, Manuel Costa, Sylvan Clebsch, Christoph M. Wintersteiger
2024	J	`jnl`	Confidential Computing Proofs: An alternative to cryptographic zero-knowledge. ACM Queue Mark Russinovich, Cédric Fournet, Greg Zaverucha, Josh Benaloh, Brandon Murdoch, Manuel Costa
2024	A*	`conf`	Gaussian Elimination of Side-Channels: Linear Algebra for Memory Coloring. CCS Jana Hofmann, Cédric Fournet, Boris Köpf, Stavros Volos
2024	A*	`conf`	Principled Microarchitectural Isolation on Cloud CPUs. CCS Stavros Volos, Cédric Fournet, Jana Hofmann, Boris Köpf, Oleksii Oleksenko
2024	J	`jnl`	Why Should I Trust Your Code? Commun. ACM Antoine Delignat-Lavaud, Cédric Fournet, Kapil Vaswani, Sylvan Clebsch, Maik Riechert, Manuel Costa, Mark Russinovich
2023	B	`conf`	ASN1*: Provably Correct, Non-malleable Parsing for ASN.1 DER. CPP Haobin Ni, Antoine Delignat-Lavaud, Cédric Fournet, Tahina Ramananandro, Nikhil Swamy
2023	—	`conf`	Confidential Computing within an AI Accelerator. USENIX ATC Kapil Vaswani, Stavros Volos, Cédric Fournet, Antonio Nino Diaz, Ken Gordon, Balaji Vembu, Sam Webster, David Chisnall, Saurabh Kulkarni, Graham Cunningham, Richard Osborne, Dan Wilkinson
2023	J	`jnl`	Confidential Consortium Framework: Secure Multiparty Applications with Confidentiality, Integrity, and High Availability. CoRR Heidi Howard, Fritz Alder, Edward Ashton, Amaury Chamayou, Sylvan Clebsch, Manuel Costa, Antoine Delignat-Lavaud, Cédric Fournet, Andrew Jeffery, Matthew Kerner, Fotios Kounelis, Markus A. Kuppe, Julien Maffre, Mark Russinovich, Christoph M. Wintersteiger
2023	J	`jnl`	Confidential Consortium Framework: Secure Multiparty Applications with Confidentiality, Integrity, and High Availability. Proc. VLDB Endow. Heidi Howard, Fritz Alder, Edward Ashton, Amaury Chamayou, Sylvan Clebsch, Manuel Costa, Antoine Delignat-Lavaud, Cédric Fournet, Andrew Jeffery, Matthew Kerner, Fotios Kounelis, Markus A. Kuppe, Julien Maffre, Mark Russinovich, Christoph M. Wintersteiger
2023	A*	`conf`	Speculation at Fault: Modeling and Testing Microarchitectural Leakage of CPU Exceptions. USENIX Security Symposium Jana Hofmann, Emanuele Vannacci, Cédric Fournet, Boris Köpf, Oleksii Oleksenko
2023	J	`jnl`	Why Should I Trust Your Code?: Confidential computing enables users to authenticate code running in TEEs, but users also need evidence this code is trustworthy. ACM Queue Antoine Delignat-Lavaud, Cédric Fournet, Kapil Vaswani, Sylvan Clebsch, Maik Riechert, Manuel Costa, Mark Russinovich
2022	J	`jnl`	Confidential Machine Learning within Graphcore IPUs. CoRR Kapil Vaswani, Stavros Volos, Cédric Fournet, Antonio Nino Diaz, Ken Gordon, Balaji Vembu, Sam Webster, David Chisnall, Saurabh Kulkarni, Graham Cunningham, Richard Osborne, Dan Wilkinson
2022	Misc	`conf`	IA-CCF: Individual Accountability for Permissioned Ledgers. NSDI Alex Shamis, Peter R. Pietzuch, Burcu Canakci, Miguel Castro, Cédric Fournet, Edward Ashton, Amaury Chamayou, Sylvan Clebsch, Antoine Delignat-Lavaud, Matthew Kerner, Julien Maffre, Olga Vrousgou, Christoph M. Wintersteiger, Manuel Costa, Mark Russinovich
2022	—	`conf`	Key-Schedule Security for the TLS 1.3 Standard. ASIACRYPT (1) Chris Brzuska, Antoine Delignat-Lavaud, Christoph Egger, Cédric Fournet, Konrad Kohbrok, Markulf Kohlweiss
2021	A*	`conf`	A Security Model and Fully Verified Implementation for the IETF QUIC Record Layer. SP Antoine Delignat-Lavaud, Cédric Fournet, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Jay Bosamiya, Joseph Lallemand, Itsaka Rakotonirina, Yi Zhou
2021	A	`conf`	AMP: authentication of media via provenance. MMSys Paul England, Henrique S. Malvar, Eric Horvitz, Jack W. Stokes, Cédric Fournet, Rebecca Burke-Aguero, Amaury Chamayou, Sylvan Clebsch, Manuel Costa, John Deutscher, Shabnam Erfani, Matt Gaylor, Andrew Jenks, Kevin Kane, Elissa M. Redmiles, Alex Shamis, Isha Sharma, John C. Simmons, Sam Wenker, Anika Zaman
2021	J	`jnl`	Key-schedule Security for the TLS 1.3 Standard. IACR Cryptol. ePrint Arch. Chris Brzuska, Antoine Delignat-Lavaud, Christoph Egger, Cédric Fournet, Konrad Kohbrok, Markulf Kohlweiss
2021	J	`jnl`	PAC: Practical Accountability for CCF. CoRR Alex Shamis, Peter R. Pietzuch, Miguel Castro, Edward Ashton, Amaury Chamayou, Sylvan Clebsch, Antoine Delignat-Lavaud, Cédric Fournet, Matthew Kerner, Julien Maffre, Manuel Costa, Mark Russinovich
2021	J	`jnl`	Toward Confidential Cloud Computing: Extending hardware-enforced cryptographic protection to data while in use. ACM Queue Mark Russinovich, Manuel Costa, Cédric Fournet, David Chisnall, Antoine Delignat-Lavaud, Sylvan Clebsch, Kapil Vaswani, Vikas Bhatia
2021	J	`jnl`	Toward confidential cloud computing. Commun. ACM Mark Russinovich, Manuel Costa, Cédric Fournet, David Chisnall, Antoine Delignat-Lavaud, Sylvan Clebsch, Kapil Vaswani, Vikas Bhatia
2020	J	`jnl`	A Security Model and Fully Verified Implementation for the IETF QUIC Record Layer. IACR Cryptol. ePrint Arch. Antoine Delignat-Lavaud, Cédric Fournet, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Jay Bosamiya, Joseph Lallemand, Itsaka Rakotonirina, Yi Zhou
2020	J	`jnl`	AMP: Authentication of Media via Provenance. CoRR Paul England, Henrique S. Malvar, Eric Horvitz, Jack W. Stokes, Cédric Fournet, Amaury Chamayou, Sylvan Clebsch, Manuel Costa, Shabnam Erfani, Kevin Kane, Alex Shamis
2020	A*	`conf`	EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider. SP 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
2019	J	`jnl`	EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider. IACR Cryptol. ePrint Arch. 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
2019	A*	`conf`	EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats. USENIX Security Symposium Tahina Ramananandro, Antoine Delignat-Lavaud, Cédric Fournet, Nikhil Swamy, Tej Chajed, Nadim Kobeissi, Jonathan Protzenko
2018	B	`conf`	A monadic framework for relational verification: applied to information security, program equivalence, and optimizations. CPP Niklas Grimm, Kenji Maillard, Cédric Fournet, Catalin Hritcu, Matteo Maffei, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Santiago Zanella-Béguelin
2018	J	`jnl`	Recalling a witness: foundations and applications of monotonic state. Proc. ACM Program. Lang. Danel Ahman, Cédric Fournet, Catalin Hritcu, Kenji Maillard, Aseem Rastogi, Nikhil Swamy
2018	—	`conf`	State Separation for Code-Based Game-Playing Proofs. ASIACRYPT (3) Chris Brzuska, Antoine Delignat-Lavaud, Cédric Fournet, Konrad Kohbrok, Markulf Kohlweiss
2018	J	`jnl`	The Applied Pi Calculus: Mobile Values, New Names, and Secure Communication. J. ACM Martín Abadi, Bruno Blanchet, Cédric Fournet
2017	J	`jnl`	A Monadic Framework for Relational Verification (Functional Pearl). CoRR Niklas Grimm, Kenji Maillard, Cédric Fournet, Catalin Hritcu, Matteo Maffei, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy, Santiago Zanella-Béguelin
2017	J	`jnl`	A messy state of the union: taming the composite state machines of TLS. Commun. ACM Benjamin Beurdouche, Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub, Jean Karim Zinzindohoue
2017	—	`conf`	Everest: Towards a Verified, Drop-in Replacement of HTTPS. SNAPL 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
2017	A*	`conf`	Implementing and Proving the TLS 1.3 Record Layer. IEEE Symposium on Security and Privacy 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
2017	J	`jnl`	Recalling a Witness: Foundations and Applications of Monotonic State. CoRR Danel Ahman, Cédric Fournet, Catalin Hritcu, Kenji Maillard, Aseem Rastogi, Nikhil Swamy
2017	J	`jnl`	Verified Low-Level Programming Embedded in F CoRR 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
2017	J	`jnl`	Verified low-level programming embedded in F. Proc. ACM Program. Lang. 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
2016	A	`conf`	A Certified Compiler for Verifiable Computing. CSF Cédric Fournet, Chantal Keller, Vincent Laporte
2016	A*	`conf`	Cinderella: Turning Shabby X.509 Certificates into Elegant Anonymous Credentials with the Magic of Verifiable Computation. IEEE Symposium on Security and Privacy Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Bryan Parno
2016	A*	`conf`	Dependent types and multi-monadic effects in F. POPL 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
2016	A*	`conf`	Downgrade Resilience in Key-Exchange Protocols. IEEE Symposium on Security and Privacy Karthikeyan Bhargavan, Christina Brzuska, Cédric Fournet, Matthew Green, Markulf Kohlweiss, Santiago Zanella-Béguelin
2016	J	`jnl`	Downgrade Resilience in Key-Exchange Protocols. IACR Cryptol. ePrint Arch. Karthikeyan Bhargavan, Christina Brzuska, Cédric Fournet, Matthew Green, Markulf Kohlweiss, Santiago Zanella-Béguelin
2016	—	`conf`	Formal Verification of Smart Contracts: Short Paper. PLAS@CCS 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
2016	A*	`conf`	Hash First, Argue Later: Adaptive Verifiable Computations on Outsourced Data. CCS Dario Fiore, Cédric Fournet, Esha Ghosh, Markulf Kohlweiss, Olga Ohrimenko, Bryan Parno
2016	J	`jnl`	Hash First, Argue Later: Adaptive Verifiable Computations on Outsourced Data. IACR Cryptol. ePrint Arch. Dario Fiore, Cédric Fournet, Esha Ghosh, Markulf Kohlweiss, Olga Ohrimenko, Bryan Parno
2016	J	`jnl`	Implementing and Proving the TLS 1.3 Record Layer. IACR Cryptol. ePrint Arch. 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
2016	A*	`conf`	Oblivious Multi-Party Machine Learning on Trusted Processors. USENIX Security Symposium Olga Ohrimenko, Felix Schuster, Cédric Fournet, Aastha Mehta, Sebastian Nowozin, Kapil Vaswani, Manuel Costa
2016	J	`jnl`	The Applied Pi Calculus: Mobile Values, New Names, and Secure Communication. CoRR Martín Abadi, Bruno Blanchet, Cédric Fournet
2016	—	`conf`	Verified Secure Implementations for the HTTPS Ecosystem: Invited Talk. PLAS@CCS Cédric Fournet
2016	J	`jnl`	miTLS: Verifying Protocol Implementations against Real-World Attacks. IEEE Secur. Priv. Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss
2015	A*	`conf`	A Messy State of the Union: Taming the Composite State Machines of TLS. IEEE Symposium on Security and Privacy Benjamin Beurdouche, Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub, Jean Karim Zinzindohoue
2015	A*	`conf`	Geppetto: Versatile Verifiable Computation. IEEE Symposium on Security and Privacy Craig Costello, Cédric Fournet, Jon Howell, Markulf Kohlweiss, Benjamin Kreuter, Michael Naehrig, Bryan Parno, Samee Zahur
2015	A	`ed.`	IEEE 28th Computer Security Foundations Symposium, CSF 2015, Verona, Italy, 13-17 July, 2015 CSF Cédric Fournet, Michael W. Hicks, Luca Viganò
2015	A*	`conf`	Observing and Preventing Leakage in MapReduce. CCS Olga Ohrimenko, Manuel Costa, Cédric Fournet, Christos Gkantsidis, Markulf Kohlweiss, Divya Sharma
2015	A*	`conf`	Safe & Efficient Gradual Typing for TypeScript. POPL Aseem Rastogi, Nikhil Swamy, Cédric Fournet, Gavin M. Bierman, Panagiotis Vekris
2015	A*	`conf`	VC3: Trustworthy Data Analytics in the Cloud Using SGX. IEEE Symposium on Security and Privacy Felix Schuster, Manuel Costa, Cédric Fournet, Christos Gkantsidis, Marcus Peinado, Gloria Mainar-Ruiz, Mark Russinovich
2014	J	`jnl`	Geppetto: Versatile Verifiable Computation. IACR Cryptol. ePrint Arch. Craig Costello, Cédric Fournet, Jon Howell, Markulf Kohlweiss, Benjamin Kreuter, Michael Naehrig, Bryan Parno, Samee Zahur
2014	A*	`conf`	Gradual typing embedded securely in JavaScript. POPL Nikhil Swamy, Cédric Fournet, Aseem Rastogi, Karthikeyan Bhargavan, Juan Chen, Pierre-Yves Strub, Gavin M. Bierman
2014	A*	`conf`	Probabilistic relational verification for cryptographic implementations. POPL Gilles Barthe, Cédric Fournet, Benjamin Grégoire, Pierre-Yves Strub, Nikhil Swamy, Santiago Zanella-Béguelin
2014	—	`conf`	Proving the TLS Handshake Secure (As It Is). CRYPTO (2) Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub, Santiago Zanella-Béguelin
2014	J	`jnl`	Proving the TLS Handshake Secure (as it is). IACR Cryptol. ePrint Arch. Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub, Santiago Zanella-Béguelin
2014	—	`conf`	Square Span Programs with Applications to Succinct NIZK Arguments. ASIACRYPT (1) George Danezis, Cédric Fournet, Jens Groth, Markulf Kohlweiss
2014	J	`jnl`	Square Span Programs with Applications to Succinct NIZK Arguments. IACR Cryptol. ePrint Arch. George Danezis, Cédric Fournet, Jens Groth, Markulf Kohlweiss
2014	A*	`conf`	Triple Handshakes and Cookie Cutters: Breaking and Fixing Authentication over TLS. IEEE Symposium on Security and Privacy Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Alfredo Pironti, Pierre-Yves Strub
2013	A*	`conf`	Fully abstract compilation to JavaScript. POPL Cédric Fournet, Nikhil Swamy, Juan Chen, Pierre-Évariste Dagand, Pierre-Yves Strub, Benjamin Livshits
2013	A*	`conf`	Implementing TLS with Verified Cryptographic Security. IEEE Symposium on Security and Privacy Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub
2013	—	`conf`	Pinocchio coin: building zerocoin from a succinct pairing-based proof system. PETShop@CCS George Danezis, Cédric Fournet, Markulf Kohlweiss, Bryan Parno
2013	J	`jnl`	Secure distributed programming with value-dependent types. J. Funct. Program. Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, Jean Yang
2013	—	`conf`	Smart meter aggregation via secret-sharing. SEGS@CCS George Danezis, Cédric Fournet, Markulf Kohlweiss, Santiago Zanella-Béguelin
2013	A*	`conf`	ZQL: A Compiler for Privacy-Preserving Data Processing. USENIX Security Symposium Cédric Fournet, Markulf Kohlweiss, George Danezis, Zhengqin Luo
2012	A*	`conf`	Self-certification: bootstrapping certified typecheckers in F* with Coq. POPL Pierre-Yves Strub, Nikhil Swamy, Cédric Fournet, Juan Chen
2012	J	`jnl`	Verified Cryptographic Implementations for TLS. ACM Trans. Inf. Syst. Secur. Karthikeyan Bhargavan, Cédric Fournet, Ricardo Corin, Eugen Zalinescu
2011	A	`conf`	Compiling Information-Flow Security to Minimal Trusted Computing Bases. ESOP Cédric Fournet, Jérémy Planul
2011	—	`conf`	Cryptographic Verification by Typing for a Sample Protocol Implementation. FOSAD Cédric Fournet, Karthikeyan Bhargavan, Andrew D. Gordon
2011	A*	`conf`	Information-flow types for homomorphic encryptions. CCS Cédric Fournet, Jérémy Planul, Tamara Rezk
2011	A*	`conf`	Modular code-based cryptographic verification. CCS Cédric Fournet, Markulf Kohlweiss, Pierre-Yves Strub
2011	J	`jnl`	Refinement types for secure implementations. ACM Trans. Program. Lang. Syst. Jesper Bengtson, Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Sergio Maffeis
2011	A	`conf`	Secure distributed programming with value-dependent types. ICFP Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, Jean Yang
2010	A*	`conf`	Modular verification of security protocol code by typing. POPL Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon
2010	—	`ch.`	Principles and Applications of Refinement Types. Logics and Languages for Reliability and Security Andrew D. Gordon, Cédric Fournet
2010	J	`jnl`	SecPAL: Design and semantics of a decentralized authorization language. J. Comput. Secur. Moritz Y. Becker, Cédric Fournet, Andrew D. Gordon
2010	B	`conf`	Typechecking Higher-Order Security Libraries. APLAS Karthikeyan Bhargavan, Cédric Fournet, Nataliya Guts
2009	A*	`conf`	A security-preserving compiler for distributed programs: from information-flow policies to cryptographic mechanisms. CCS Cédric Fournet, Gurvan Le Guernic, Tamara Rezk
2009	A	`conf`	Cryptographic Protocol Synthesis and Verification for Multiparty Sessions. CSF Karthikeyan Bhargavan, Ricardo Corin, Pierre-Malo Deniélou, Cédric Fournet, James J. Leifer
2009	A	`conf`	Reliable Evidence: Auditability by Typing. ESORICS Nataliya Guts, Cédric Fournet, Francesco Zappa Nardelli
2009	B	`conf`	Secure Enforcement for Global Process Specifications. CONCUR Jérémy Planul, Ricardo Corin, Cédric Fournet
2008	A	`conf`	A Formal Implementation of Value Commitment. ESOP Cédric Fournet, Nataliya Guts, Francesco Zappa Nardelli
2008	J	`jnl`	A secure compiler for session abstractions. J. Comput. Secur. Ricardo Corin, Pierre-Malo Deniélou, Cédric Fournet, Karthikeyan Bhargavan, James J. Leifer
2008	J	`jnl`	Automated verification of selected equivalences for security protocols. J. Log. Algebraic Methods Program. Bruno Blanchet, Martín Abadi, Cédric Fournet
2008	A	`conf`	Code-Carrying Authorization. ESORICS Sergio Maffeis, Martín Abadi, Cédric Fournet, Andrew D. Gordon
2008	A*	`conf`	Cryptographically sound implementations for typed information-flow security. POPL Cédric Fournet, Tamara Rezk
2008	A*	`conf`	Cryptographically verified implementations for TLS. CCS Karthikeyan Bhargavan, Cédric Fournet, Ricardo Corin, Eugen Zalinescu
2008	A	`conf`	Refinement Types for Secure Implementations. CSF Jesper Bengtson, Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Sergio Maffeis
2008	—	`ed.`	Trustworthy Global Computing, Third Symposium, TGC 2007, Sophia-Antipolis, France, November 5-6, 2007, Revised Selected Papers TGC Gilles Barthe, Cédric Fournet
2008	A	`conf`	Verified implementations of the information card federated identity-management protocol. AsiaCCS Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Nikhil Swamy
2008	J	`jnl`	Verified interoperable implementations of security protocols. ACM Trans. Program. Lang. Syst. Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Stephen Tse
2008	J	`jnl`	Verifying policy-based web services security. ACM Trans. Program. Lang. Syst. Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon
2007	A	`conf`	A Type Discipline for Authorization in Distributed Systems. CSF Cédric Fournet, Andy Gordon, Sergio Maffeis
2007	J	`jnl`	A type discipline for authorization policies. ACM Trans. Program. Lang. Syst. Cédric Fournet, Andrew D. Gordon, Sergio Maffeis
2007	A	`conf`	Design and Semantics of a Decentralized Authorization Language. CSF Moritz Y. Becker, Cédric Fournet, Andrew D. Gordon
2007	J	`jnl`	Just fast keying in the pi calculus. ACM Trans. Inf. Syst. Secur. Martín Abadi, Bruno Blanchet, Cédric Fournet
2007	A	`conf`	Secure Implementations for Typed Session Abstractions. CSF Ricardo Corin, Pierre-Malo Deniélou, Cédric Fournet, Karthikeyan Bhargavan, James J. Leifer
2007	J	`jnl`	Secure sessions for Web services. ACM Trans. Inf. Syst. Secur. Karthikeyan Bhargavan, Ricardo Corin, Cédric Fournet, Andrew D. Gordon
2006	B	`conf`	Computational Secrecy by Typing for the Pi Calculus. APLAS Martín Abadi, Ricardo Corin, Cédric Fournet
2006	—	`conf`	Cryptographically Sound Implementations for Communicating Processes. ICALP (2) Pedro Adão, Cédric Fournet
2006	—	`conf`	Verified Interoperable Implementations of Security Protocols. CSFW Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Stephen Tse
2006	—	`conf`	Verified Reference Implementations of WS-Security Protocols. WS-FM Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon
2005	A	`conf`	A Type Discipline for Authorization Policies. ESOP Cédric Fournet, Andrew D. Gordon, Sergio Maffeis
2005	J	`jnl`	A hierarchy of equivalences for asynchronous calculi. J. Log. Algebraic Methods Program. Cédric Fournet, Georges Gonthier
2005	J	`jnl`	A semantics for web services authentication. Theor. Comput. Sci. Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon
2005	—	`conf`	An advisor for web services security policies. SWS Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Greg O'Shea
2005	A*	`conf`	Automated Verification of Selected Equivalences for Security Protocols. LICS Bruno Blanchet, Martín Abadi, Cédric Fournet
2004	A*	`conf`	A semantics for web services authentication. POPL Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon
2004	B	`conf`	Ethernet Topology Discovery without Network Assistance. ICNP Richard Black, Austin Donnelly, Cédric Fournet
2004	—	`conf`	From Stack Inspection to Access Control: A Security Analysis for Libraries. CSFW Frédéric Besson, Tomasz Blanc, Cédric Fournet, Andrew D. Gordon
2004	A	`conf`	Just Fast Keying in the Pi Calculus. ESOP Martín Abadi, Bruno Blanchet, Cédric Fournet
2004	J	`jnl`	Modern concurrency abstractions for C#. ACM Trans. Program. Lang. Syst. Nick Benton, Luca Cardelli, Cédric Fournet
2004	J	`jnl`	Private authentication. Theor. Comput. Sci. Martín Abadi, Cédric Fournet
2004	—	`conf`	Secure sessions for web services. SWS Karthikeyan Bhargavan, Ricardo Corin, Cédric Fournet, Andrew D. Gordon
2004	A*	`conf`	Stuck-Free Conformance. CAV Cédric Fournet, C. A. R. Hoare, Sriram K. Rajamani, Jakob Rehof
2004	J	`jnl`	TulaFale: A Security Tool for Web Services CoRR Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Riccardo Pucella
2004	A*	`conf`	Verifying policy-based security for web services. CCS Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon
2003	A*	`conf`	Access Control Based on Execution History. NDSS Martín Abadi, Cédric Fournet
2003	J	`jnl`	Inheritance in the join calculus. J. Log. Algebraic Methods Program. Cédric Fournet, Cosimo Laneve, Luc Maranget, Didier Rémy
2003	J	`jnl`	Stack inspection: Theory and variants. ACM Trans. Program. Lang. Syst. Cédric Fournet, Andrew D. Gordon
2003	—	`conf`	TulaFale: A Security Tool for Web Services. FMCO Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Riccardo Pucella
2002	—	`conf`	Hiding Names: Private Authentication in the Applied Pi Calculus. ISSS Cédric Fournet, Martín Abadi
2002	—	`conf`	JoCaml: A Language for Concurrent Distributed and Mobile Programming. Advanced Functional Programming Cédric Fournet, Fabrice Le Fessant, Luc Maranget, Alan Schmitt
2002	A	`conf`	Modern Concurrency Abstractions for C ECOOP Nick Benton, Luca Cardelli, Cédric Fournet
2002	J	`jnl`	Secure Implementation of Channel Abstractions. Inf. Comput. Martín Abadi, Cédric Fournet, Georges Gonthier
2002	A*	`conf`	Stack inspection: theory and variants. POPL Cédric Fournet, Andrew D. Gordon
2001	J	`jnl`	Bisimulations in the join-calculus. Theor. Comput. Sci. Cédric Fournet, Cosimo Laneve
2001	A*	`conf`	Mobile values, new names, and secure communication. POPL Martín Abadi, Cédric Fournet
2000	—	`conf`	An Asynchronous, Distributed Implementation of Mobile Ambients. IFIP TCS Cédric Fournet, Jean-Jacques Lévy, Alan Schmitt
2000	A*	`conf`	Authentication Primitives and Their Compilation. POPL Martín Abadi, Cédric Fournet, Georges Gonthier
2000	—	`conf`	Inheritance in the Join Calculus. FSTTCS Cédric Fournet, Cosimo Laneve, Luc Maranget, Didier Rémy
2000	—	`conf`	The Join Calculus: A Language for Distributed Mobile Programming. APPSEM Cédric Fournet, Georges Gonthier
1999	—	`conf`	A Top-Down Look at a Secure Message. FSTTCS Martín Abadi, Cédric Fournet, Georges Gonthier
1999	—	`conf`	Secure Communications Processing for Distributed Languages. S&P Martín Abadi, Cédric Fournet, Georges Gonthier
1998	A*	`conf`	A Hierarchy of Equivalences for Asynchronous Calculi. ICALP Cédric Fournet, Georges Gonthier
1998	—	`conf`	Bisimulations in the join-calculus. PROCOMET Michele Boreale, Cédric Fournet, Cosimo Laneve
1998	A*	`conf`	Secure Implementation of Channel Abstractions. LICS Martín Abadi, Cédric Fournet, Georges Gonthier
1997	B	`conf`	Implicit Typing à la ML for the Join-Calculus. CONCUR Cédric Fournet, Cosimo Laneve, Luc Maranget, Didier Rémy
1997	—	`conf`	Secure Implementation of Channel Abstractions. HOOTS Martín Abadi, Cédric Fournet, Georges Gonthier
1996	B	`conf`	A Calculus of Mobile Agents. CONCUR Cédric Fournet, Georges Gonthier, Jean-Jacques Lévy, Luc Maranget, Didier Rémy
1996	A*	`conf`	The Reflexive CHAM and the Join-Calculus. POPL Cédric Fournet, Georges Gonthier