Sites Inria

Version française

PROSECCO Research team

PROSECCO team publications

2018

Journal articles

titre
Gradual liquid type inference
auteur
Niki Vazou, Eric Tanter, David Van Horn
article
Proceedings of the ACM on Programming Languages, ACM, 2018, 2 (OOPSLA), pp.1-25. <10.1145/3276502>
Accès au bibtex
https://arxiv.org/pdf/1807.02132 BibTex
titre
Equivalences for Free
auteur
Nicolas Tabareau, Éric Tanter, Matthieu Sozeau
article
Proceedings of the ACM on Programming Languages, ACM, 2018, ICFP'18, pp.1-29. <10.1145/3234615>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01559073/file/main_icfp.pdf BibTex
titre
Graduality from embedding-projection pairs
auteur
Max New, Amal Ahmed
article
Proceedings of the ACM on Programming Languages, ACM, 2018, 2 (ICFP), pp.1-30. <10.1145/3236768>
Accès au bibtex
https://arxiv.org/pdf/1807.02786 BibTex
titre
Recalling a Witness: Foundations and Applications of Monotonic State
auteur
Danel Ahman, Cédric Fournet, Cătălin Hriţcu, Kenji Maillard, Aseem Rastogi, Nikhil Swamy
article
Proceedings of the ACM on Programming Languages, ACM, 2018, 2 (POPL), <10.1145/3158153>
Accès au bibtex
https://arxiv.org/pdf/1707.02466 BibTex
titre
Handling Fibred Algebraic Effects
auteur
Danel Ahman
article
Proceedings of the ACM on Programming Languages, ACM, 2018, 2 (POPL), <10.1145/3158095>
Accès au bibtex
BibTex
titre
Type‐Preserving CPS Translation of Σ and Π Types is Not Not Possible
auteur
William J. Bowman, Youyou Cong, Nick Rioux, Amal Ahmed
article
Proceedings of the ACM on Programming Languages, ACM, 2018, 2 (POPL), <10.1145/3158110>
Accès au bibtex
BibTex
titre
Automated reasoning for equivalences in the applied pi calculus with barriers
auteur
Bruno Blanchet, Ben Smyth
article
Journal of Computer Security, IOS Press, 2018, 26 (3), pp.367 - 422. <10.3233/JCS-171013>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01947972/file/JCS.pdf BibTex

Conference papers

titre
When Good Components Go Bad
auteur
Carmine Abate, Arthur Azevedo de Amorim, Roberto Blanco, Ana Nora Evans, Guglielmo Fachini, Cătălin Hriţcu, Théo Laurent, Benjamin C. Pierce, Marco Stronati, Andrew Tolmach
article
25th ACM Conference on Computer and Communications Security (CCS), Oct 2018, Toronto, Canada. ACM, pp.1351--1368, 2018, <10.1145/3243734.3243745>
Accès au bibtex
https://arxiv.org/pdf/1802.00588 BibTex
titre
A Hypersequent Calculus with Clusters for Linear Frames
auteur
David Baelde, Anthony Lick, Sylvain Schmitz
article
Guram Bezhanishvili; Giovanna D'Agostino; George Metcalfe; Thomas Studer. Twefth Conference on Advances in Modal Logic, Jul 2018, Bern, Switzerland. College Publications, 12, pp.36--55, 2018, Advances in Modal Logic
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01756126/file/main.pdf BibTex
titre
Composition Theorems for CryptoVerif and Application to TLS 1.3
auteur
Bruno Blanchet
article
31st IEEE Computer Security Foundations Symposium (CSF'18), Jul 2018, Oxford, United Kingdom. 2018, <10.1109/CSF.2018.00009>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01947959/file/BlanchetCSF18.pdf BibTex
titre
Typed closure conversion for the calculus of constructions
auteur
William Bowman, Amal Ahmed
article
Proceedings of 39th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’18), Jun 2018, Philadelphia, PA, United States. <10.1145/3296979.3192372>
Accès au bibtex
https://arxiv.org/pdf/1808.04006 BibTex
titre
A Formal Treatment of Accountable Proxying over TLS
auteur
Karthikeyan Bhargavan, Ioana Boureanu, Antoine Delignat-Lavaud, Pierre-Alain Fouque, Cristina Onete
article
2018 IEEE Symposium on Security and Privacy (SP) (2018), May 2018, San Francisco, United States
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01948722/file/main.pdf BibTex
titre
Ledger Design Language: Designing and Deploying Formally Verified Public Ledgers
auteur
Nadim Kobeissi, Natalia Kulatova
article
Workshop on Security Protocol Implementations: Development and Analysis, Apr 2018, London, United Kingdom
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01948971/file/ldl_short.pdf BibTex
titre
The Meaning of Memory Safety
auteur
Arthur Azevedo de Amorim, Cătălin Hriţcu, Benjamin C. Pierce
article
7th International Conference on Principles of Security and Trust (POST), Apr 2018, Thessaloniki, Greece. pp.79--105, 2018, <10.1007/978-3-319-89722-6_4>
Accès au bibtex
https://arxiv.org/pdf/1705.07354 BibTex
titre
FabULous Interoperability for ML and a Linear Language
auteur
Gabriel Scherer, Max New, Nick Rioux, Amal Ahmed
article
Christel Baier; Ugo Dal Lago. International Conference on Foundations of Software Science and Computation Structures (FoSSaCS), Apr 2018, Thessaloniki, Greece. Springer, LNCS - Lecture Notes in Computer Science (10803), FabOpen image in new windowous Interoperability for ML and a Linear Language. <10.1007/978-3-319-89366-2_8>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01929158/file/1707.04984.pdf BibTex
titre
Noise Explorer: Fully Automated Modeling and Verification for Arbitrary Noise Protocols
auteur
Nadim Kobeissi, Karthikeyan Bhargavan
article
Real World Cryptography Symposium, Jan 2018, San Jose, United States
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01948964/file/noise.pdf BibTex
titre
A Monadic Framework for Relational Verification
auteur
Niklas Grimm, Kenji Maillard, Cédric Fournet, Cătălin Hriţcu, Matteo Maffei, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Santiago Zanella‐béguelin
article
7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP), Jan 2018, Los Angeles, United States. ACM, pp.130--145, 2018, <10.1145/3167090>
Accès au bibtex
https://arxiv.org/pdf/1703.00055 BibTex
titre
A Hypersequent Calculus with Clusters for Tense Logic over Ordinals
auteur
David Baelde, Anthony Lick, Sylvain Schmitz
article
Sumit Ganguly and Paritosh Pandya. 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2018, Ahmedabad, India. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 122, pp.15:1--15:19, Leibniz International Proceedings in Informatics. <10.4230/LIPIcs.FSTTCS.2018.15>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01852077/file/main.pdf BibTex

Reports

titre
Composition Theorems for CryptoVerif and Application to TLS 1.3
auteur
Bruno Blanchet
article
[Research Report] RR-9171, Inria Paris. 2018, pp.67
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01764527/file/RR-9171.pdf BibTex

Preprints, Working Papers, ...

titre
Capsule: A Protocol for Secure Collaborative Document Editing
auteur
Nadim Kobeissi
article
2018
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01948967/file/spec.pdf BibTex
titre
Decidable XPath Fragments in the Real World
auteur
David Baelde, Anthony Lick, Sylvain Schmitz
article
2018
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01852475/file/main.pdf BibTex

2017

Journal articles

titre
The Applied Pi Calculus: Mobile Values, New Names, and Secure Communication
auteur
Martín Abadi, Bruno Blanchet, Cédric Fournet
article
Journal of the ACM (JACM), Association for Computing Machinery, 2017, 65 (1), pp.1 - 103. <10.1145/3127586>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01636616/file/eqns.pdf BibTex
titre
Systematizing Decentralization and Privacy: Lessons from 15 Years of Research and Deployments
auteur
Carmela Troncoso, Marios Isaakidis, George Danezis, Harry Halpin
article
Proceedings on Privacy Enhancing Technologies, De Gruyter Open, 2017, 2017 (4), pp.307 - 329. <10.1515/popets-2017-0056>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01673295/file/paper87-2017-4-source.pdf BibTex
titre
Verified Low‐Level Programming Embedded in F*
auteur
Jonathan Protzenko, Jean‐karim Zinzindohoué, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella‐béguelin, Antoine Delignat‐lavaud, Cătălin Hriţcu, Karthikeyan Bhargavan, Cédric Fournet, Nikhil Swamy
article
Proceedings of the ACM on Programming Languages, ACM, 2017, 1 (ICFP), pp.17:1--17:29. <10.1145/3110261>
Accès au bibtex
https://arxiv.org/pdf/1703.00053 BibTex
titre
A Reduced Semantics for Deciding Trace Equivalence
auteur
Stéphanie Delaune, David Baelde, Lucca Hirschi
article
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2017, 13 (2), pp.1-48. <10.23638/LMCS-13(2:8)2017>
Accès au bibtex
BibTex
titre
A messy state of the union: taming the composite state machines of TLS
auteur
Karthikeyan Bhargavan, Benjamin Beurdouche, Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub, Jean Karim Zinzindohoue
article
Communications of the ACM, ACM, 2017, 60 (2), pp.99 - 107. <10.1145/3023357>
Accès au bibtex
BibTex
titre
Correctness of Speculative Optimizations with Dynamic Deoptimization
auteur
Olivier Flückiger, Gabriel Scherer, Ming-Ho Yee, Aviral Goel, Amal Ahmed, Jan Vitek
article
Proceedings of the ACM on Programming Languages, ACM, In press, <10.1145/3158137>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01646765/file/sourir.pdf BibTex

Conference papers

titre
The Crisis of Standardizing DRM: The Case of W3C Encrypted Media Extensions
auteur
Harry Halpin
article
SPACE 2017 - Seventh International Conference on Security, Privacy, and Applied Cryptography Engineering, Dec 2017, Goa, India. Springer, 10662, pp.10-29, Lecture Notes in Computer Science. <10.1007/978-3-319-71501-8_2>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01673296/file/drm.pdf BibTex
titre
Security Analysis of the W3C Web Cryptography API
auteur
Kelsey Cairns, Harry Halpin, Graham Steel
article
Proceedings of Security Standardisation Research (SSR), Dec 2017, Gaithersberg, United States. Springer, 10074, pp.112 - 140, 2016, Lecture Notes in Computer Science (LNCS). . <10.1007/978-3-319-49100-4_5>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01426852/file/main-hal2.pdf BibTex
titre
HACL * : A Verified Modern Cryptographic Library
auteur
Jean-Karim Zinzindohoué, Karthikeyan Bhargavan, Jonathan Protzenko, Benjamin Beurdouche
article
ACM Conference on Computer and Communications Security (CCS), Oct 2017, Dallas, United States.
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01588421/file/haclstar.pdf BibTex
titre
A Roadmap for High Assurance Cryptography
auteur
Harry Halpin
article
FPS 2017 - 10th International Symposium on Foundations & Practice of Security, Oct 2017, Nancy, France. pp.1-9
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01673294/file/paper.pdf BibTex
titre
Semantic Insecurity: Security and the Semantic Web
auteur
Harry Halpin
article
PrivOn 2017 - Workshop Society, Privacy and the Semantic Web - Policy and Technology, Oct 2017, Vienna, Austria. pp.1-10,
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01673291/file/main.pdf BibTex
titre
NEXTLEAP: Decentralizing Identity with Privacy for Secure Messaging
auteur
Harry Halpin
article
ARES 2017 - 12th International Conference on Availability, Reliability and Security, Aug 2017, Reggio Calabria, Italy. ACM, ARES '17 Proceedings of the 12th International Conference on Availability, Reliability and Security, pp.1-10, 2017, . <10.1145/3098954.3104056>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01673292/file/ares2017.pdf BibTex
titre
Symbolic and Computational Mechanized Verification of the ARINC823 Avionic Protocols
auteur
Bruno Blanchet
article
30th IEEE Computer Security Foundations Symposium, Aug 2017, Santa Barbara, United States. pp.68-82, 2017, <10.1109/CSF.2017.7>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01575861/file/BlanchetCSF17.pdf BibTex
titre
Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate
auteur
Karthikeyan Bhargavan, Bruno Blanchet, Nadim Kobeissi
article
38th IEEE Symposium on Security and Privacy, May 2017, San Jose, United States. pp.483 - 502, 2017, <10.1109/SP.2017.26>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01575920/file/paper.pdf BibTex
titre
Implementing and Proving the TLS 1.3 Record Layer
auteur
Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Jianyang Pan, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy, Santiago Zanella-Béguelin, Jean Zinzindohoué
article
SP 2017 - 38th IEEE Symposium on Security and Privacy, May 2017, San Jose, United States. pp.463-482, 2017, <10.1109/SP.2017.58>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01674096/file/record.pdf BibTex
titre
Everest: Towards a Verified, Drop‐in Replacement of HTTPS
auteur
Karthikeyan Bhargavan, Barry Bond, Antoine Delignat‐lavaud, Cédric Fournet, Chris Hawblitzel, Catalin Hritcu, Samin Ishtiaq, Markulf Kohlweiss, Rustan Leino, Jay Lorch, Kenji Maillard, Jianyang Pain, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Ashay Rane, Aseem Rastogi, Nikhil Swamy, Laure Thompson, Perry Wang, Santiago Zanella‐béguelin, Jean Karim Zinzindohoué
article
2nd Summit on Advances in Programming Languages (SNAPL), May 2017, Asilomar, CA, United States. 2017, <10.4230/LIPIcs.SNAPL.2017.1>
Accès au bibtex
BibTex
titre
Taking Updates Seriously
auteur
Danel Ahman, Tarmo Uustalu
article
Proceedings of the 6th International Workshop on Bidirectional Transformations co‐located with The European Joint Conferences on Theory and Practice of Software - ETAPS 2017, Apr 2017, Uppsala, Sweden. pp.59--73, 2017
Accès au bibtex
BibTex
titre
Automated Verification for Secure Messaging Protocols and Their Implementations: A Symbolic and Computational Approach
auteur
Nadim Kobeissi, Karthikeyan Bhargavan, Bruno Blanchet
article
2nd IEEE European Symposium on Security and Privacy , Apr 2017, Paris, France. pp.435 - 450, 2017, . <10.1109/EuroSP.2017.38>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01575923/file/KobeissiBhargavanBlanchetEuroSP17.pdf BibTex
titre
Automated Verification for Secure Messaging Protocols and their Implementations: A Symbolic and Computational Approach
auteur
Nadim Kobeissi, Karthikeyan Bhargavan, Bruno Blanchet
article
IEEE European Symposium on Security and Privacy, Apr 2017, Paris, France
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01948965/file/paper-longversion.pdf BibTex
titre
On the Practical (In-)Security of 64-bit Block Ciphers
auteur
Gaëtan Leurent, Karthikeyan Bhargavan
article
ESC 2017 - Early Symmetric Crypto, Jan 2017, Canach, Luxembourg.
Accès au bibtex
BibTex
titre
Beginner's Luck: A Language for Random Generators
auteur
Leonidas Lampropoulos, Diane Gallois-Wong, Cătălin Hriţcu, John Hughes, Benjamin C. Pierce, Li-Yao Xia
article
44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), 2017, Paris, France. ACM, pp.114-129, 2017, <10.1145/3009837.3009868>
Accès au bibtex
https://arxiv.org/pdf/1607.05443 BibTex
titre
Dijkstra Monads for Free
auteur
Danel Ahman, Cătălin Hriţcu, Kenji Maillard, Guido Martínez, Gordon Plotkin, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy
article
44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), 2017, Paris, France. ACM, pp.515-529, 2017, <10.1145/3009837.3009878>
Accès au bibtex
https://arxiv.org/pdf/1608.06499 BibTex

Documents associated with scientific events

titre
Introduction to Security and Privacy on the Blockchain
auteur
Harry Halpin, Marta Piekarska
article
EuroS&P 2017 - 2nd IEEE European Symposium on Security and Privacy, Workshops, Apr 2017, Paris, France. IEEE, Security and Privacy Workshops (EuroS&PW), 2017 IEEE European Symposium on, pp.1-3, 2017, . <10.1109/EuroSPW.2017.43>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01673293/file/intro_final.pdf BibTex
titre
Content Delivery over TLS: A Cryptographic Analysis of Keyless SSL
auteur
Karthikeyan Bhargavan, Ioana Boureanu, Pierre-Alain Fouque, Cristina Onete, Benjamin Richard
article
EuroS&P 2017 - 2nd IEEE European Symposium on Security and Privacy, Apr 2017, Paris, France. IEEE, 2017 IEEE European Symposium on Security and Privacy (EuroS&P), pp.600-615, 2017, . <10.1109/EuroSP.2017.52>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01673853/file/main.pdf BibTex

Reports

titre
Symbolic and Computational Mechanized Verification of the ARINC823 Avionic Protocols
auteur
Bruno Blanchet
article
[Research Report] RR-9072, Inria Paris. 2017, pp.40
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01527671/file/RR-9072.pdf BibTex
titre
Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate
auteur
Karthikeyan Bhargavan, Bruno Blanchet, Nadim Kobeissi
article
[Research Report] RR-9040, Inria Paris. 2017, pp.51
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01528752/file/RR-9040.pdf BibTex

Theses

titre
A formalization of elliptic curves for cryptography
auteur
Evmorfia-Iro Bartzia
article
Cryptography and Security [cs.CR]. Université Paris-Saclay, 2017. English.
Accès au texte intégral et bibtex
https://pastel.archives-ouvertes.fr/tel-01563979/file/43038_BARTZIA_2017_archivage.pdf BibTex

2016

Journal articles

titre
miTLS: Verifying Protocol Implementations against Real-World Attacks
auteur
Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss
article
IEEE Security & Privacy, IEEE, 2016, 14 (6), pp.18-25. <10.1109/MSP.2016.123>
Accès au bibtex
BibTex
titre
The Decentralization of Knowledge
auteur
Harry Halpin, Alexandre Monnin
article
First Monday, University of Illinois at Chicago Library, 2016, “Reclaiming the Internet” with distributed architectures, 21 (12), . <10.5210/fm.v21i12.7109>
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01397931/file/First%20Monday%20Decentralization%20of%20Knowledge.pdf BibTex
titre
A Verified Information-Flow Architecture
auteur
Arthur Azevedo de Amorim, Nathan Collins, André Dehon, Delphine Demange, Cătălin Hriţcu, David Pichardie, Benjamin C. Pierce, Randy Pollack, Andrew Tolmach
article
Journal of Computer Security, IOS Press, 2016, 24 (6), pp.689--734. <10.3233/JCS-15784>
Accès au bibtex
https://arxiv.org/pdf/1509.06503 BibTex
titre
Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif
auteur
Bruno Blanchet
article
Foundations and Trends® in Privacy and Security , Now publishers inc, 2016, 1 (1-2), pp.1 - 135. <10.1561/3300000004>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01423760/file/proverif.pdf BibTex
titre
Testing Noninterference, Quickly
auteur
Cătălin Hriţcu, Leonidas Lampropoulos, Antal Spector-Zabusky, Arthur Azevedo Amorim, Maxime Dénès, John Hughes, Benjamin C. Pierce, Dimitrios Vytiniotis
article
Journal of Functional Programming (JFP); Special issue for ICFP 2013, 2016, 26, e4 (62 p.). <10.1017/S0956796816000058>
Accès au bibtex
https://arxiv.org/pdf/1409.0393 BibTex

Conference papers

titre
LEAP: A next-generation client VPN and encrypted email provider
auteur
Elijah Sparrow, Harry Halpin, Kali Kaneko, Ruben Pollan
article
Sara Foresti; Giuseppe Persiano. CANS 2016 - 15th International Conference Cryptology and Network Security, Nov 2016, Milan, Italy. Springer, 10052, pp.176 - 191, 2016, Lecture Notes in Computer Science (LNCS). . <10.1007/978-3-319-48965-0_11>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01426850/file/cans2016.pdf BibTex
titre
Formal Verification of Smart Contracts: Short Paper
auteur
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
article
ACM Workshop on Programming Languages and Analysis for Security, Oct 2016, Vienna, Austria. Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security, 2016, <10.1145/2993600.2993611>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01400469/file/solidether.pdf BibTex
titre
On the Practical (In-)Security of 64-bit Block Ciphers
auteur
Karthikeyan Bhargavan, Gaëtan Leurent
article
ACM CCS 2016 - 23rd ACM Conference on Computer and Communications Security, Oct 2016, Vienna, Austria. ACM; ACM Press, pp.456-467, 2016, . <10.1145/2976749.2978423>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01404208/file/SWEET32_CCS16.pdf BibTex
titre
UnlimitID
auteur
Marios Isaakidis, Harry Halpin, George Danezis
article
Proceedings of the 2016 ACM on Workshop on Privacy in the Electronic Society, Oct 2016, Vienna, Austria. pp.139 - 142, 2016, WPES. . <10.1145/2994620.2994637>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01426847/file/WPES2016_paper_56_camerready.pdf BibTex
titre
End-to-End Encrypted Messaging Protocols: An Overview
auteur
Ksenia Ermoshina, Francesca Musiani, Harry Halpin
article
Franco Bagnoli ; Anna Satsiou; Ioannis Stavrakakis; Paolo Nesi ; Giovanna Pacini; Yanina Welp ; Thanassis Tiropanis ; Dominic DiFranzo Third International Conference, INSCI 2016 - Internet Science, Sep 2016, Florence, Italy. Springer, 9934, pp.244 - 254, 2016, Lecture Notes in Computer Science (LNCS). <10.1007/978-3-319-45982-0_22>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01426845/file/paper_21.pdf BibTex
titre
The Responsibility of Open Standards in the Era of Surveillance
auteur
Harry Halpin
article
Hot Topics in Privacy Enchancing Technologies, Jul 2016, Darmstadt, Germany. HotPETS.
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01426848/file/halpin-hotpets2016-v2.pdf BibTex
titre
A Verified Extensible Library of Elliptic Curves
auteur
Jean Karim Zinzindohoue, Evmorfia-Iro Bartzia, Karthikeyan Bhargavan
article
29th IEEE Computer Security Foundations Symposium (CSF), Jun 2016, Lisboa, Portugal. IEEE Computer Security Foundations Symposium (CSF 2016), 2016, <10.1109/CSF.2016.28>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01425957/file/paper.pdf BibTex
titre
Automated Reasoning for Equivalences in the Applied Pi Calculus with Barriers
auteur
Bruno Blanchet, Ben Smyth
article
29th IEEE Computer Security Foundations Symposium (CSF'16), Jun 2016, Lisboa, Portugal. pp.310 - 324, 2016, <10.1109/CSF.2016.29>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01423742/file/BlanchetSmythCSF16.pdf BibTex
titre
Downgrade Resilience in Key-Exchange Protocols
auteur
Karthikeyan Bhargavan, Chris Brzuska, Cédric Fournet, Matthew Green, Markulf Kohlweiss, Santiago Zanella-Béguelin
article
IEEE Symposium on Security and Privacy (SP), 2016 , May 2016, San Jose, United States. <10.1109/SP.2016.37>
Accès au bibtex
BibTex
titre
Transcript Collision Attacks: Breaking Authentication in TLS, IKE, and SSH
auteur
Karthikeyan Bhargavan, Gaëtan Leurent
article
Network and Distributed System Security Symposium -- NDSS 2016, Feb 2016, San Diego, United States. <10.14722/ndss.2016.23418>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01244855/file/SLOTH_NDSS16.pdf BibTex
titre
Dependent Types and Multi-Monadic Effects in F*
auteur
Nikhil Swamy, Cătălin Hriţcu, 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
article
43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 2016, St. Petersburg, Florida, United States. ACM, pp.256-270, 2016, <10.1145/2837614.2837655>
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01265793/file/paper.pdf BibTex
titre
Beyond Good and Evil: Formalizing the Security Guarantees of Compartmentalizing Compilation
auteur
Yannis Juglaret, Cătălin Hriţcu, Arthur Azevedo Amorim, Boris Eng, Benjamin C. Pierce
article
29th IEEE Symposium on Computer Security Foundations (CSF), 2016, Lisabon, Portugal. IEEE Computer Society Press, pp.45--60, 2016, <10.1109/CSF.2016.11>
Accès au bibtex
https://arxiv.org/pdf/1602.04503 BibTex

Reports

titre
Formal Modeling and Verification for Domain Validation and ACME
auteur
Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Nadim Kobeissi
article
[Research Report] INRIA Paris; Microsoft Research Cambridge. 2016
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01397439/file/paper.pdf BibTex
titre
The Applied Pi Calculus: Mobile Values, New Names, and Secure Communication
auteur
Martín Abadi, Bruno Blanchet, Cédric Fournet
article
[Research Report] ArXiv. 2016, pp.110
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01423924/file/eqns-article.pdf BibTex
titre
Automated reasoning for equivalences in the applied pi calculus with barriers
auteur
Bruno Blanchet, Ben Smyth
article
[Research Report] RR-8906, Inria Paris. 2016, pp.54
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01306440/file/RR-8906.pdf BibTex

Theses

titre
On the security of authentication protocols on the web
auteur
Antoine Delignat-Lavaud
article
Cryptography and Security [cs.CR]. PSL Research University, 2016. English.
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-01469937/file/thesisDelignatLavaud.pdf BibTex

2015

Journal articles

titre
Proved Generation of Implementations from Computationally Secure Protocol Specifications
auteur
David Cadé, Bruno Blanchet
article
Journal of Computer Security, IOS Press, 2015, 23 (3), pp.331-402
Accès au bibtex
BibTex

Conference papers

titre
Imperfect Forward Secrecy: How Diffie-Hellman Fails in Practice
auteur
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
article
ACM CCS 2015, Oct 2015, Denver, Colorado, United States. Proceedings of the 2015 ACM SIGSAC Conference on Computer and Communications Security, pp.14, 2015 ACM SIGSAC Conference on Computer and Communications Security. <10.1145/2810103.2813707>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01184171/file/logjam.pdf BibTex
titre
Foundational Property-Based Testing
auteur
Zoe Paraskevopoulou, Cătălin Hriţcu, Maxime Dénès, Leonidas Lampropoulos, Benjamin C. Pierce
article
ITP 2015 - 6th conference on Interactive Theorem Proving, Aug 2015, Nanjing, China. Springer, 9236, 2015, Lecture Notes in Computer Science. <10.1007/978-3-319-22102-1_22>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01162898/file/main.pdf BibTex
titre
Network-based Origin Confusion Attacks against HTTPS Virtual Hosting
auteur
Antoine Delignat-Lavaud, Karthikeyan Bhargavan
article
24th International Conference on World Wide Web, May 2015, Florence, Italy. ACM, 2015,
Accès au bibtex
BibTex
titre
A Messy State of the Union: Taming the Composite State Machines of TLS
auteur
Benjamin Beurdouche, Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub, Jean Karim Zinzindohoue
article
IEEE Symposium on Security & Privacy 2015, May 2015, San Jose, United States. IEEE, 2015
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01114250/file/messy-state-of-the-union-oakland15.pdf BibTex
titre
Micro-Policies: Formally Verified, Tag-Based Security Monitors
auteur
Arthur Azevedo de Amorim, Maxime Dénès, Nick Giannarakis, Cătălin Hriţcu, Benjamin Pierce, Antal Spector-Zabusky, Andrew Tolmach
article
2015 IEEE Symposium on Security and Privacy, May 2015, San Jose, United States. pp.813 - 830, 2015, 2015 IEEE Symposium on Security and Privacy. <10.1109/SP.2015.55>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01265666/file/micro-policies.pdf BibTex
titre
Architectural Support for Software-Defined Metadata Processing
auteur
Udit Dhawan, Cătălin Hriţcu, Rafi Rubin, Nikos Vasilakis, Silviu Chiricescu, Jonathan M. Smith, Jr. Thomas F. Knight, Benjamin C. Pierce, André Dehon
article
20th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS 2015), Mar 2015, Istanbul, Turkey. ACM, pp.487-502, 2015, <10.1145/2694344.2694383>
Accès au bibtex
BibTex
titre
Verified Contributive Channel Bindings for Compound Authentication
auteur
Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Alfredo Pironti
article
Network and Distributed System Security Symposium (NDSS'15), Feb 2015, San Diego, United States. 2015
Accès au bibtex
BibTex

Reports

titre
From the Applied Pi Calculus to Horn Clauses for Protocols with Lists
auteur
Miriam Paiola, Bruno Blanchet
article
[Research Report] RR-8823, Inria. 2015, pp.45
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01239290/file/RR-8823.pdf BibTex

2014

Journal articles

titre
Formal verification of security protocol implementations: a survey
auteur
Matteo Avalle, Alfredo Pironti, Riccardo Sisto
article
Formal Aspects of Computing, Springer Verlag, 2014, 26 (1), pp.99-123. <10.1007/s00165-012-0269-9>
Accès au bibtex
BibTex
titre
Union, Intersection, and Refinement Types and Reasoning About Type Disjointness for Secure Protocol Implementations
auteur
Michael Backes, Cătălin Hriţcu, Matteo Maffei
article
Journal of Computer Security, IOS Press, 2014, 22 (2), pp.301-353. <10.3233/JCS-130493>
Accès au bibtex
BibTex
titre
Discovering concrete attacks on website authorization by formal analysis
auteur
Chetan Bansal, Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Sergio Maffeis
article
Journal of Computer Security, IOS Press, 2014, 22 (4), pp.601-657. <10.3233/JCS-140503>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01102202/file/JCS.pdf BibTex
titre
A Generic Security API for Symmetric Key Management on Cryptographic Devices
auteur
Véronique Cortier, Graham Steel
article
Information and Computation, Elsevier, 2014, 238, pp.25
Accès au bibtex
BibTex

Conference papers

titre
A Computationally Complete Symbolic Attacker for Equivalence Properties
auteur
Gergei Bana, Hubert Comon-Lundh
article
2014 ACM SIGSAC Conference on Computer and Communications Security, Nov 2014, Scottsdale, United States. ACM, pp.609-620, 2014, <10.1145/2660267.2660276>
Accès au bibtex
BibTex
titre
Proving the TLS Handshake Secure (as it is)
auteur
Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub, Santiago Zanella-Béguelin
article
Juan A. Garay; Rosario Gennaro. CRYPTO 2014, Aug 2014, Santa Barbara, United States. Springer, 8617, pp.235-255, 2014, Lecture Notes in Computer Science. <10.1007/978-3-662-44381-1_14>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01102229/file/182.pdf BibTex
titre
FLEXTLS A Tool for Testing TLS Implementations
auteur
Benjamin Beurdouche, Antoine Delignat-Lavaud, Nadim Kobeissi, Alfredo Pironti, Karthikeyan Bhargavan
article
9th USENIX Workshop on Offensive Technologies, WOOT '15, Aug 2014, Washington DC, United States
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01295035/file/woot15-paper-beurdouche.pdf BibTex
titre
Beagle as a HOL4 external ATP method
auteur
Thibault Gauthier, Cezary Kaliszyk, Chantal Keller, Michael Norrish
article
PAAR - Fourth Workshop on Practical Aspects of Automated Reasoning, Jul 2014, Vienne, Austria. 2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01089316/file/beagle-hol4.pdf BibTex
titre
A Formal Library for Elliptic Curves in the Coq Proof Assistant
auteur
Evmorfia-Iro Bartzia, Pierre-Yves Strub
article
Gerwin Klein; Ruben Gamboa. Interactive Theorem Proving, Jul 2014, Vienna, Austria. Springer, 8558, pp.77-92, 2014, Lecture Notes in Computer Science. <10.1007/978-3-319-08970-6_6>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01102288/file/A-Formal-Library-for-Elliptic-Curves-in-the-Coq-Proof-Assistant.pdf BibTex
titre
Automated Analysis of Security Protocols with Global State
auteur
Steve Kremer, Robert Künnemann
article
IEEE Computer Society. 35th IEEE Symposium on Security and Privacy (S&P'14), May 2014, San Jose, United States. pp.163-178, Proceedings of the 35th IEEE Symposium on Security and Privacy (S&P'14). <10.1109/SP.2014.18>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01091241/file/KK-sp14.pdf BibTex
titre
Triple Handshakes and Cookie Cutters: Breaking and Fixing Authentication over TLS
auteur
Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Alfredo Pironti, Pierre-Yves Strub
article
IEEE Symposium on Security & Privacy, Apr 2014, San Jose, United States. IEEE, <10.1109/SP.2014.14>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01102259/file/triple-handshakes-and-cookie-cutters-oakland14.pdf BibTex
titre
Hawk and Aucitas: e-Auction Schemes from the Helios and Civitas e-Voting Schemes
auteur
Adam Mccarthy, Ben Smyth, Elizabeth A. Quaglia
article
Nicolas Christin; Reihaneh Safavi-Naini. FC 2014 - Financial Cryptography and Data Security, Mar 2014, Christ Church, Barbados. Springer, 8437, pp.51-63, 2014, LNCS - Lecture Notes in Computer Science. <10.1007/978-3-662-45472-5_4>
Accès au bibtex
BibTex
titre
Web PKI: Closing the Gap between Guidelines and Practices
auteur
Antoine Delignat-Lavaud, Martin Abadí, Matthew Birrell, Ilya Mironov, Ted Wobber, Yinglian Xie
article
Network and Distributed System Security Symposium, Feb 2014, San Diego, United States. Internet Society, 2014, <10.14722/ndss.2014.23305>
Accès au bibtex
BibTex
titre
Gradual Typing Embedded Securely in JavaScript
auteur
Nikhil Swamy, Cédric Fournet, Aseem Rastogi, Karthikeyan Bhargavan, Juan Chen, Pierre-Yves Strub, Gavin Bierman
article
POPL 2014 - 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Jan 2014, San Diego, CA, United States. ACM, pp.425-437, 2014, <10.1145/2535838.2535889>
Accès au bibtex
BibTex
titre
Computationally Complete Symbolic Adversary and Key Exchange
auteur
Gergei Bana, Koji Hasebe, Mitsuhiro Okada
article
31st Symposium on Cryptography and Information Security, 2014, Kagoshima, Japan. 2014
Accès au bibtex
BibTex
titre
A Verified Information-Flow Architecture
auteur
Arthur Azevedo de Amorim, Nathan Collins, André Dehon, Delphine Demange, Catalin Hritcu, David Pichardie, Benjamin C. Pierce, Randy Pollack, Andrew Tolmach
article
41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 2014, San Diego, CA, United States. 2014, <10.1145/2535838.2535839>
Accès au bibtex
BibTex

Book sections

titre
A secure key management interface with asymmetric cryptography
auteur
Marion Daubignard, David Lubicz, Graham Steel
article
Martin Abadi; Steve kremer. Principles of Security and Trust: Third International Conference, POST 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings , 8414, Springer, pp.63-82, 2014, Lecture notes in computer science, 978-3-642-54791-1. <10.1007/978-3-642-54792-8_4>
Accès au bibtex
BibTex
titre
Automatic Verification of Security Protocols in the Symbolic Model: The Verifier ProVerif
auteur
Bruno Blanchet
article
Alessandro Aldini; Javier Lopez; Fabio Martinelli. Foundations of Security Analysis and Design VII, 8604, Springer, pp.54-87, 2014, Lecture Notes in Computer Science, 978-3-319-10081-4. <10.1007/978-3-319-10082-1_3>
Accès au bibtex
BibTex
titre
Defensive JavaScript
auteur
Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Sergio Maffeis
article
Alessandro Aldini; Javier Lopez; Fabio Martinelli. Foundations of Security Analysis and Design VII, 8604, Springer, pp.88-123, 2014, Lecture Notes in Computer Science, 978-3-319-10081-4. <10.1007/978-3-319-10082-1_4>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01102144/file/djs-tutorial.pdf BibTex

Reports

titre
Truncating TLS Connections to Violate Beliefs in Web Applications
auteur
Ben Smyth, Alfredo Pironti
article
[Research Report] INRIA Paris. 2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01102013/file/main-tls-logout.pdf BibTex
titre
Ballot secrecy with malicious bulletin boards
auteur
Ben Smyth, David Bernhard
article
[Research Report] 2014/822, Cryptology ePrint Archive. 2014, pp.7
Accès au bibtex
BibTex
titre
Testing Noninterference, Quickly
auteur
Cătălin Hriţcu, Leonidas Lampropoulos, Antal Spector-Zabusky, Arthur Azevedo De Amorim, Maxime Dénès, John Hughes, Benjamin C. Pierce, Dimitrios Vytiniotis
article
[Research Report] arXiv:1409.0393, arXiv. 2014, pp.50
Accès au bibtex
https://arxiv.org/pdf/1409.0393 BibTex
titre
Proving the TLS Handshake Secure (as it is)
auteur
Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub, Santiago Zanella-Béguelin
article
[Research Report] 2014/182, Cryptology ePrint Archive. 2014, pp.48
Accès au bibtex
BibTex

Theses

titre
Verification of cryptographic protocols with lists of unbounded lengths
auteur
Miriam Paiola
article
Cryptography and Security [cs.CR]. Université Paris-Diderot (Paris 7), 2014. English
Accès au texte intégral et bibtex
https://hal.inria.fr/tel-01103104/file/thesis%281%29.pdf BibTex

2013

Journal articles

titre
Verification of Security Protocols with Lists: from Length One to Unbounded Length
auteur
Miriam Paiola, Bruno Blanchet
article
Journal of Computer Security, IOS Press, 2013, 21 (6), pp.781--816
Accès au bibtex
BibTex
titre
Secure Distributed Programming with Value-Dependent Types
auteur
Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, Jean Yang
article
J. Funct. Program., Cambridge University Press, 2013, 23 (4), pp.402-451
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00939188/file/secure-distributed-programming-with-value-dependent-types-jfp-1.pdf BibTex
titre
From Computationally-Proved Protocol Specifications to Implementations and Application to SSH
auteur
David Cadé, Bruno Blanchet
article
Journal of Wireless Mobile Networks, Ubiquitous Computing, and Dependable Applications (JoWUA), Innovative Information Science & Technology Research Group (ISYOU), 2013, 4 (1), pp.4--31
Accès au bibtex
BibTex

Conference papers

titre
Computationally Complete Symbolic Attacker and Key Exchange
auteur
Gergei Bana, Koji Hasebe, Mitsuhiro Okada
article
CCS 2013 - 20th ACM Conference on Computer and Communications Security, Nov 2013, Berlin, Germany. ACM, CCS '13 Proceedings of the 2013 ACM SIGSAC conference on Computer & communications security, pp.1231-1246, 2013, <10.1145/2508859.2516710>
Accès au bibtex
BibTex
titre
Automatic Verification of Protocols with Lists of Unbounded Length
auteur
Bruno Blanchet, Miriam Paiola
article
CCS'13 - ACM Conference on Computer and Communications Security, Nov 2013, Berlin, Germany. ACM, pp.573--584, 2013, <10.1145/2508859.2516679>
Accès au bibtex
BibTex
titre
Language-Based Defenses Against Untrusted Browser Origins
auteur
Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Sergio Maffeis
article
Proceedings of the 22th USENIX Security Symposium, Aug 2013, Washington, D.C., United States. 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00863372/file/language-based-defenses-against-untrusted-origins-sec13.pdf BibTex
titre
Proving More Observational Equivalences with ProVerif
auteur
Vincent Cheval, Bruno Blanchet
article
David Basin and John Mitchell. POST 2013 - 2nd Conference on Principles of Security and Trust, Mar 2013, Rome, Italy. Springer, LNCS, 7796, pp.226-246, 2013, POST 2013: Principles of Security and Trust. <10.1007/978-3-642-36830-1_12>
Accès au bibtex
BibTex
titre
Towards Unified Authorization for Android
auteur
Michael J. May, Karthikeyan Bhargavan
article
5th International Symposium on Engineering Secure Software and Systems (ESSoS 2013), Feb 2013, Rocquencourt, France. spv, 7781, pp.42-57, 2013, llncs
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00863384/file/towards-unified-authorization-for-android-essos13.pdf BibTex
titre
Universally Composable Key-Management
auteur
Steve Kremer, Robert Künnemann, Graham Steel
article
Crampton, Jason and Jajodia, Sushil. 18th European Symposium on Research in Computer Security (ESORICS'13), 2013, Egham, United Kingdom. Springer, 8134, 2013, Lecture Notes in Computer Science. <10.1007/978-3-642-40203-6_19>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00878632/file/KKS-esorics13.pdf BibTex
titre
Implementing TLS with Verified Cryptographic Security
auteur
Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub
article
IEEE Symposium on Security & Privacy, 2013, San Francisco, United States. pp.445-462, 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00863373/file/implementing-tls-with-verified-cryptographic-security-oakland13.pdf BibTex
titre
Keys to the Cloud: Formal Analysis and Concrete Attacks on Encrypted Web Storage
auteur
Chetan Bansal, Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Sergio Maffeis
article
David Basin and John Mitchell. 2nd Conference on Principles of Security and Trust (POST 2013), 2013, Rome, Italy. spv, 7796, pp.126--146, 2013, lncs
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00863375/file/keys-to-the-cloud-post13.pdf BibTex
titre
Proved Generation of Implementations from Computationally-Secure Protocol Specifications
auteur
David Cadé, Bruno Blanchet
article
David Basin and John Mitchell. 2nd Conference on Principles of Security and Trust (POST 2013), 2013, Rome, Italy. spv, 7796, pp.63--82, 2013, lncs
Accès au bibtex
BibTex
titre
Ballot secrecy and ballot independence coincide
auteur
Ben Smyth, David Bernhard
article
ESORICS'13: 18th European Symposium on Research in Computer Security, 2013, Egham, United Kingdom. Springer, 8134, pp.463-480, 2013, LNCS
Accès au bibtex
BibTex
titre
Truncating TLS Connections to Violate Beliefs in Web Applications
auteur
Ben Smyth, Alfredo Pironti
article
WOOT'13: 7th USENIX Workshop on Offensive Technologies, 2013, Washington, United States. USENIX Association, 2013
Accès au bibtex
BibTex

Reports

titre
Ballot secrecy and ballot independence: definitions and relations
auteur
Ben Smyth, David Bernhard
article
[Research Report] 2013/235, Cryptology ePrint Archive. 2013, pp.24
Accès au bibtex
BibTex
titre
Discovering Concrete Attacks on Website Authorization by Formal Analysis
auteur
Chetan Bansal, Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Sergio Maffeis
article
[Research Report] RR-8287, INRIA. 2013, pp.46
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00815834/file/oauth.pdf BibTex
titre
Embedding of Security Components in Untrusted Third-Party Websites
auteur
Antoine Delignat-Lavaud, Karthikeyan Bhargavan, Sergio Maffeis
article
[Research Report] RR-8285, INRIA. 2013, pp.32
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00815800/file/tech.pdf BibTex
titre
A Secure Key Management Interface with Asymmetric Cryptography
auteur
Marion Daubignard, David Lubicz, Graham Steel
article
[Research Report] RR-8274, INRIA. 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00805987/file/asym_API_RR.pdf BibTex

Theses

titre
Proved Implementations of Cryptographic Protocols in the Computational Model
auteur
David Cadé
article
Cryptography and Security [cs.CR]. Paris 7, 2013. English
Accès au texte intégral et bibtex
https://hal.inria.fr/tel-01112630/file/main.pdf BibTex

2012

Journal articles

titre
Formally-Based Semi-Automatic Implementation of an Open Security Protocol
auteur
Alfredo Pironti, Davide Pozza, Riccardo Sisto
article
Journal of Systems and Software, Elsevier, 2012, 85 (4), pp.835-849. <10.1016/j.jss.2011.10.052>
Accès au bibtex
BibTex
titre
Safe Abstractions of Data Encodings in Formal Security Protocol Models
auteur
Alfredo Pironti, Riccardo Sisto
article
Formal Aspects of Computing, Springer Verlag, 2012, pp.1-43
Accès au bibtex
BibTex
titre
Verified Cryptographic Implementations for TLS
auteur
Karthikeyan Bhargavan, Ricardo Corin, Cédric Fournet, Eugen Zalinescu
article
ACM Transactions on Information and System Security, Association for Computing Machinery, 2012, 15 (1), pp.3:1--3:32. <10.1145/2133375.2133378>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00863381/file/cryptographically-verified-implementations-for-tls-tissec.pdf BibTex

Conference papers

titre
Visual Model-Driven Design, Verification and Implementation of Security Protocols
auteur
Piergiuseppe Bettassa Copet, Alfredo Pironti, Davide Pozza, Riccardo Sisto, Pietro Vivoli
article
HASE 2012 - IEEE 14th International Symposium on High Assurance Systems Engineering, Oct 2012, Omaha, United States. IEEE Computer Security, High-Assurance Systems Engineering (HASE), 2012 IEEE 14th International Symposium on, pp.62-65, 2012, <10.1109/HASE.2012.23>
Accès au bibtex
BibTex
titre
Revoke and Let Live: A Secure Key Revocation API for Cryptographic Devices
auteur
Véronique Cortier, Graham Steel, Cyrille Wiedling
article
19th ACM Conference on Computer and Communications Security (CCS'12), Oct 2012, Raleigh, United States. ACM, 2012
Accès au bibtex
BibTex
titre
Web-based Attacks on Host-Proof Encrypted Storage
auteur
Karthikeyan Bhargavan, Antoine Delignat-Lavaud
article
6th USENIX Workshop on Offensive Technologies (WOOT'12), Aug 2012, Bellevue, WA, United States. pp.97--104, 2012
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00863383/file/host_proof_woot12.pdf BibTex
titre
Discovering Concrete Attacks on Website Authorization by Formal Analysis
auteur
Chetan Bansal, Karthikeyan Bhargavan, Sergio Maffeis
article
25th IEEE Computer Security Foundations Symposium (CSF'12), 2012, Cambridge, MA, United States. pp.247--262, 2012
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00863385/file/discovering_concrete_attacks_csf12.pdf BibTex
titre
Efficient Padding Oracle Attacks on Cryptographic Hardware
auteur
Romain Bardou, Riccardo Focardi, Yusuke Kawamoto, Lorenzo Simionato, Graham Steel, Joe-Kai Tsay
article
CRYPTO, 2012, Unknown, Afghanistan. pp.608--625, 2012
Accès au bibtex
BibTex
titre
YubiSecure? Formal Security Analysis Results for the Yubikey and YubiHSM
auteur
Robert Künnemann, Graham Steel
article
Jøsang, Audun and Samarati, Pierangela and Petrocchi, Marinella. Revised Selected Papers of the 8th Workshop on Security and Trust Management (STM'12), 2012, Pisa, Italy. Springer, 7783, pp.257-272, 2012, Lecture Notes in Computer Science. <10.1007/978-3-642-38004-4_17>
Accès au bibtex
BibTex
titre
Automatically Verified Mechanized Proof of One-Encryption Key Exchange
auteur
Bruno Blanchet
article
25th IEEE Computer Security Foundations Symposium (CSF'12), 2012, Cambridge, United States. pp.325--339, 2012
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00863386/file/BlanchetCSF12.pdf BibTex
titre
Verification of Security Protocols with Lists: from Length One to Unbounded Length
auteur
Miriam Paiola, Bruno Blanchet
article
Pierpaolo Degano and Joshua Guttman. First Conference on Principles of Security and Trust (POST'12), 2012, Tallinn, Estonia. spv, 7215, pp.69--88, 2012, lncs
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00863387/file/PaiolaBlanchetPOST12LV.pdf BibTex
titre
Security Protocol Verification: Symbolic and Computational Models
auteur
Bruno Blanchet
article
Pierpaolo Degano and Joshua Guttman. First Conference on Principles of Security and Trust (POST'12), 2012, Tallinn, Estonia. spv, 7215, pp.3--29, 2012, lncs
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00863388/file/BlanchetETAPS12.pdf BibTex
titre
Computationally Complete Symbolic Attacker in Action
auteur
Gergei Bana, Pedro Ad Ao, Hideki Sakurada
article
IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012), 2012, Unknown, Afghanistan. 2012, Leibniz International Proceedings in Informatics (LIPIcs)
Accès au bibtex
BibTex
titre
Towards Unconditional Soundness: Computationally Complete Symbolic Attacker
auteur
Gergei Bana, Hubert Comon-Lundh
article
2nd Conference on Principles of Security and Trust (POST 2012), 2012, Unknown, spv, 7215, pp.189-208, 2012, llncs
Accès au bibtex
BibTex
titre
From Computationally-proved Protocol Specifications to Implementations
auteur
David Cadé, Bruno Blanchet
article
7th International Conference on Availability, Reliability and Security (AReS 2012), 2012, Prague, Czech Republic. IEEE, pp.65--74, 2012
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00863382/file/CadeBlanchetARES12.pdf BibTex

Book sections

titre
Mechanizing Game-Based Proofs of Security Protocols
auteur
Bruno Blanchet
article
Tobias Nipkow and Olga Grumberg and Benedikt Hauptmann. Software Safety and Security - Tools for Analysis and Verification, 33, IOS Press, pp.1--25, 2012, NATO Science for Peace and Security Series ― D: Information and Communication Security
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00863389/file/BlanchetMOD11.pdf BibTex

Reports

titre
Identifying Website Users by TLS Traffic Analysis: New Attacks and Effective Countermeasures
auteur
Alfredo Pironti, Pierre-Yves Strub, Karthikeyan Bhargavan
article
[Research Report] RR-8067, INRIA. 2012
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00732449/file/RR-8067.pdf BibTex
titre
Revoke and Let Live: A Secure Key Revocation API for Cryptographic Devices
auteur
Véronique Cortier, Graham Steel, Cyrille Wiedling
article
[Research Report] RR-7949, INRIA. 2012, pp.41
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00721945/file/RR-7949.pdf BibTex
titre
Efficient Padding Oracle Attacks on Cryptographic Hardware
auteur
Romain Bardou, Riccardo Focardi, Yusuke Kawamoto, Lorenzo Simionato, Graham Steel, Joe-Kai Tsay
article
[Research Report] RR-7944, INRIA. 2012, pp.19
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00691958/file/RR-7944.pdf BibTex

2011

Book sections

titre
Cryptographic Verification by Typing for a Sample Protocol Implementation
auteur
Cédric Fournet, Karthikeyan Bhargavan, Andrew Gordon
article
Alessandro Aldini; Roberto Gorrieri Cryptographic Verification by Typing for a Sample Protocol Implementation, 6858, Springer, 2011, LNCS - Lecture Notes in Computer Science, 978-3-642-23081-3. <10.1007/978-3-642-23082-0_3>
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01295013/file/cryptographic_verification_fosad10.pdf BibTex