Biography

I am in the Prosecco team at Inria Paris. I am interested in the application of formal methods in security. I work on proofs of security protocols (in particular of authentication and privacy properties), the application of automated deduction techniques to help automate protocol analysis, and the usage of static analysis in security.

The web-page of the Squirrel Prover: https://squirrel-prover.github.io/

Publications

(2024). Foundations for Cryptographic Reductions in CCSA Logics. 2024 ACM SIGSAC Conference on Computer and Communications Security, CCS'24.

PDF

(2024). A Probabilistic Logic for Concrete Security. IEEE Computer Security Foundations Symposium, CSF 2024, Enschede, Netherlands, July, 2024.

PDF Long version

(2024). The Squirrel Prover and its Logic. ACM SIGLOG News.

PDF

(2023). Mechanized Proofs of Adversarial Complexity and Application to Universal Composability. ACM TOPS, Transactions on Privacy and Security.

PDF DOI Long version

(2023). A Higher-Order Indistinguishability Logic for Cryptographic Reasoning. ACM/IEEE Symposium on Logic in Computer Science, LICS'23.

PDF

(2022). Semantic Foundations for Cost Analysis of Pipeline-Optimized Programs. SAS 2022.

PDF Long version

(2022). Cracking the Stateful Nut: Computational Proofs of Stateful Security Protocols using the Squirrel Proof Assistant . IEEE Computer Security Foundations Symposium, CSF 2022, Haifa, Israel, August, 2022.

PDF Slides

(2021). Mechanized Proofs of Adversarial Complexity and Application to Universal Composability. 2021 ACM SIGSAC Conference on Computer and Communications Security, CCS'21.

PDF Slides

(2021). An Interactive Prover for Protocol Verification in the Computational Model. IEEE Symposium on Security and Privacy, S&P 2021, San Fransisco / Virtual, United States.

PDF Slides Long version

(2021). High-Assurance Cryptography in the Spectre Era. IEEE Symposium on Security and Privacy, S&P 2021, San Fransisco / Virtual, United States.

PDF

(2020). The Last Mile: High-Assurance and High-Speed Cryptographic Implementations. IEEE Symposium on Security and Privacy.

PDF

(2019). Decidability of a Sound Set of Inference Rules for Computational Indistinguishability. 32nd IEEE Computer Security Foundations Symposium, CSF 2019, Hoboken, NJ, USA, June 25-28, 2019.

PDF Slides DOI Long version

(2019). The 5G-AKA Authentication Protocol Privacy. IEEE European Symposium on Security and Privacy, EuroS&P 2019, Stockholm, Sweden, June 17-19, 2019.

PDF Slides DOI Long version

(2017). A Sound Flow-Sensitive Heap Abstraction for the Static Analysis of Android Applications. 30th IEEE Computer Security Foundations Symposium, CSF 2017, Santa Barbara, CA, USA, August 21-25, 2017.

PDF DOI Long version

(2017). Formal Computational Unlinkability Proofs of RFID Protocols. 30th IEEE Computer Security Foundations Symposium, CSF 2017, Santa Barbara, CA, USA, August 21-25, 2017.

PDF Slides DOI

(2017). Process-centric views of data-driven business artifacts. J. Comput. Syst. Sci..

PDF DOI

(2015). Process-Centric Views of Data-Driven Business Artifacts. 18th International Conference on Database Theory, ICDT 2015, March 23-27, 2015, Brussels, Belgium.

PDF DOI

Talks

Mechanizing and Automating Cryptographic Arguments

Invited talk, ProTeCS workshop

Mechanized Proofs of Adversarial Complexity and Application to UC

SCOT seminar 15/12/2023

Verifying Cryptographic Protocols

Demi-heure de science 09/11/2023

Cracking the Stateful Nut

CSF 2022

The 5G-AKA Authentication Protocol Privacy

STIC Doctoral School Best Scientific Contribution Award Ceremony

The 5G-AKA Authentication Protocol Privacy

Prosecco Seminar

Contact