• Morio K and Künnemann R. SpecMon: Modular Black-Box Runtime Monitoring of Security Protocols. Proceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security. (2741-2755).

    https://doi.org/10.1145/3658644.3690197

  • Dupressoir F and Zain S. (2021). Machine-Checking Unforgeability Proofs for Signature Schemes with Tight Reductions to the Computational Diffie-Hellman Problem 2021 IEEE 34th Computer Security Foundations Symposium (CSF). 10.1109/CSF51468.2021.00014. 978-1-7281-7607-9. (1-15).

    https://ieeexplore.ieee.org/document/9505217/

  • Baumann C, Dam M, Guanciale R and Nemati H. (2021). On Compositional Information Flow Aware Refinement 2021 IEEE 34th Computer Security Foundations Symposium (CSF). 10.1109/CSF51468.2021.00010. 978-1-7281-7607-9. (1-16).

    https://ieeexplore.ieee.org/document/9505191/

  • Delignat-Lavaud A, Fournet C, Parno B, Protzenko J, Ramananandro T, Bosamiya J, Lallemand J, Rakotonirina I and Zhou Y. (2021). A Security Model and Fully Verified Implementation for the IETF QUIC Record Layer 2021 IEEE Symposium on Security and Privacy (SP). 10.1109/SP40001.2021.00039. 978-1-7281-8934-5. (1162-1178).

    https://ieeexplore.ieee.org/document/9519466/

  • Barbosa M, Barthe G, Bhargavan K, Blanchet B, Cremers C, Liao K and Parno B. (2021). SoK: Computer-Aided Cryptography 2021 IEEE Symposium on Security and Privacy (SP). 10.1109/SP40001.2021.00008. 978-1-7281-8934-5. (777-795).

    https://ieeexplore.ieee.org/document/9519449/

  • Barthe G, Betarte G, Campo J, Luna C and Pichardie D. (2020). System-Level Non-interference of Constant-Time Cryptography. Part II: Verified Static Analysis and Stealth Memory. Journal of Automated Reasoning. 10.1007/s10817-020-09548-x.

    http://link.springer.com/10.1007/s10817-020-09548-x

  • Almeida J, Barbosa M, Barthe G, Laporte V and Oliveira T. (2020). Certified Compilation for Cryptography: Extended x86 Instructions and Constant-Time Verification. Progress in Cryptology – INDOCRYPT 2020. 10.1007/978-3-030-65277-7_6. (107-127).

    http://link.springer.com/10.1007/978-3-030-65277-7_6

  • Almeida J, Baritel-Ruet C, Barbosa M, Barthe G, Dupressoir F, Grégoire B, Laporte V, Oliveira T, Stoughton A and Strub P. Machine-Checked Proofs for Cryptographic Standards. Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security. (1607-1622).

    https://doi.org/10.1145/3319535.3363211

  • Baek J, Susilo W, Kim J and Chow Y. Subversion in Practice: How to Efficiently Undermine Signatures. IEEE Access. 10.1109/ACCESS.2019.2918550. 7. (68799-68811).

    https://ieeexplore.ieee.org/document/8721046/

  • K. K, Rebeiro C and Hazra A. (2018). An Algorithmic Approach to Formally Verify an ECC Library. ACM Transactions on Design Automation of Electronic Systems. 23:5. (1-26). Online publication date: 18-Oct-2018.

    https://doi.org/10.1145/3224205

  • Sisto R, Bettassa Copet P, Avalle M and Pironti A. (2018). Formally sound implementations of security protocols with JavaSPI. Formal Aspects of Computing. 30:2. (279-317). Online publication date: 1-Mar-2018.

    https://doi.org/10.1007/s00165-017-0449-8

  • Almeida J, Barbosa M, Barthe G, Dupressoir F, Grégoire B, Laporte V and Pereira V. A Fast and Verified Software Stack for Secure Function Evaluation. Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security. (1989-2006).

    https://doi.org/10.1145/3133956.3134017

  • Cortier V, Dragan C, Dupressoir F, Schmidt B, Strub P and Warinschi B. (2017). Machine-Checked Proofs of Privacy for Electronic Voting Protocols 2017 IEEE Symposium on Security and Privacy (SP). 10.1109/SP.2017.28. 978-1-5090-5533-3. (993-1008).

    http://ieeexplore.ieee.org/document/7958621/

  • Zinzindohoue J, Bartzia E and Bhargavan K. (2016). A Verified Extensible Library of Elliptic Curves 2016 IEEE 29th Computer Security Foundations Symposium (CSF). 10.1109/CSF.2016.28. 978-1-5090-2607-4. (296-309).

    https://ieeexplore.ieee.org/document/7536383/

  • Fournet C, Keller C and Laporte V. (2016). A Certified Compiler for Verifiable Computing 2016 IEEE 29th Computer Security Foundations Symposium (CSF). 10.1109/CSF.2016.26. 978-1-5090-2607-4. (268-280).

    https://ieeexplore.ieee.org/document/7536381/

  • Beringer L, Petcher A, Ye K and Appel A. Verified correctness and security of OpenSSL HMAC. Proceedings of the 24th USENIX Conference on Security Symposium. (207-221).

    /doi/10.5555/2831143.2831157

  • Petcher A and Morrisett G. A Mechanized Proof of Security for Searchable Symmetric Encryption. Proceedings of the 2015 IEEE 28th Computer Security Foundations Symposium. (481-494).

    https://doi.org/10.1109/CSF.2015.36

  • Cadé D and Blanchet B. Proved generation of implementations from computationally secure protocol specifications1. Journal of Computer Security. 10.3233/JCS-150524. 23:3. (331-402).

    https://www.medra.org/servlet/aliasResolver?alias=iospress&doi=10.3233/JCS-150524

  • Appel A. (2015). Verification of a Cryptographic Primitive. ACM Transactions on Programming Languages and Systems. 37:2. (1-31). Online publication date: 16-Apr-2015.

    https://doi.org/10.1145/2701415

  • Petcher A and Morrisett G. The Foundational Cryptography Framework. Proceedings of the 4th International Conference on Principles of Security and Trust - Volume 9036. (53-72).

    https://doi.org/10.1007/978-3-662-46666-7_4

  • Cheval V and Cortier V. Timing Attacks in Security Protocols. Proceedings of the 4th International Conference on Principles of Security and Trust - Volume 9036. (280-299).

    https://doi.org/10.1007/978-3-662-46666-7_15

  • Barthe G, Crespo J, Lakhnech Y and Schmidt B. (2015). Mind the Gap: Modular Machine-Checked Proofs of One-Round Key Exchange Protocols. Advances in Cryptology - EUROCRYPT 2015. 10.1007/978-3-662-46803-6_23. (689-718).

    http://link.springer.com/10.1007/978-3-662-46803-6_23

  • Vanspauwen G and Jacobs B. (2015). Verifying Protocol Implementations by Augmenting Existing Cryptographic Libraries with Specifications. Software Engineering and Formal Methods. 10.1007/978-3-319-22969-0_4. (53-68).

    http://link.springer.com/10.1007/978-3-319-22969-0_4

  • Chen Y, Hsu C, Lin H, Schwabe P, Tsai M, Wang B, Yang B and Yang S. Verifying Curve25519 Software. Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security. (299-309).

    https://doi.org/10.1145/2660267.2660370

  • Barthe G, Betarte G, Campo J, Luna C and Pichardie D. System-level Non-interference for Constant-time Cryptography. Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security. (1267-1279).

    https://doi.org/10.1145/2660267.2660283

  • Barthe G, Dupressoir F, Fouque P, Grégoire B, Tibouchi M and Zapalowicz J. Making RSA---PSS Provably Secure against Non-random Faults. Proceedings of the 16th International Workshop on Cryptographic Hardware and Embedded Systems --- CHES 2014 - Volume 8731. (206-222).

    https://doi.org/10.1007/978-3-662-44709-3_12

  • Barthe G, Fournet C, Grégoire B, Strub P, Swamy N and Zanella-Béguelin S. (2014). Probabilistic relational verification for cryptographic implementations. ACM SIGPLAN Notices. 49:1. (193-205). Online publication date: 13-Jan-2014.

    https://doi.org/10.1145/2578855.2535847

  • Barthe G, Fournet C, Grégoire B, Strub P, Swamy N and Zanella-Béguelin S. Probabilistic relational verification for cryptographic implementations. Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. (193-205).

    https://doi.org/10.1145/2535838.2535847

  • Barthe G, Dupressoir F, Grégoire B, Kunz C, Schmidt B and Strub P. (2014). EasyCrypt: A Tutorial. Foundations of Security Analysis and Design VII. 10.1007/978-3-319-10082-1_6. (146-166).

    http://link.springer.com/10.1007/978-3-319-10082-1_6

  • Barthe G. Computer-Aided security proofs. Proceedings of the 10th international conference on Quantitative Evaluation of Systems. (1-2).

    https://doi.org/10.1007/978-3-642-40196-1_1