• Bacelar Almeida J, Firsov D, Oliveira T and Unruh D. Leakage-Free Probabilistic Jasmin Programs. Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs. (3-16).

    https://doi.org/10.1145/3703595.3705871

  • Barbosa M, Dupressoir F, Hülsing A, Meijers M and Strub P. (2025). A Tight Security Proof for SPHINCS$$^{+}$$, Formally Verified. Advances in Cryptology – ASIACRYPT 2024. 10.1007/978-981-96-0894-2_2. (35-67).

    https://link.springer.com/10.1007/978-981-96-0894-2_2

  • Samyuktha M, Borkar P and Rebeiro C. (2025). High Speed High Assurance Implementations of Multivariate Quadratic Based Signatures. Security, Privacy, and Applied Cryptography Engineering. 10.1007/978-3-031-80408-3_12. (196-200).

    https://link.springer.com/10.1007/978-3-031-80408-3_12

  • Almeida J, Arranz Olmos S, Barbosa M, Barthe G, Dupressoir F, Grégoire B, Laporte V, Léchenet J, Low C, Oliveira T, Pacheco H, Quaresma M, Schwabe P and Strub P. Formally Verifying Kyber. Advances in Cryptology – CRYPTO 2024. (384-421).

    https://doi.org/10.1007/978-3-031-68379-4_12

  • Mohamadi H, Lahlou L, Kara N and Leivadeas A. (2024). A versatile chaotic cryptosystem with a novel substitution-permutation scheme for internet-of-drones photography. Nonlinear Dynamics. 10.1007/s11071-024-09306-3. 112:6. (4977-5012). Online publication date: 1-Mar-2024.

    https://link.springer.com/10.1007/s11071-024-09306-3

  • Gregersen S, Aguirre A, Haselwarter P, Tassarotti J and Birkedal L. (2024). Asynchronous Probabilistic Couplings in Higher-Order Separation Logic. Proceedings of the ACM on Programming Languages. 8:POPL. (753-784). Online publication date: 5-Jan-2024.

    https://doi.org/10.1145/3632868

  • Hwang V. (2024). Formal Verification of Emulated Floating-Point Arithmetic in Falcon. Advances in Information and Computer Security. 10.1007/978-981-97-7737-2_7. (125-141).

    https://link.springer.com/10.1007/978-981-97-7737-2_7

  • Lai L, Liu J, Shi X, Tsai M, Wang B and Yang B. (2024). Automatic Verification of Cryptographic Block Function Implementations with Logical Equivalence Checking. Computer Security – ESORICS 2024. 10.1007/978-3-031-70903-6_19. (377-395).

    https://link.springer.com/10.1007/978-3-031-70903-6_19

  • Haselwarter P, Rivas E, Van Muylder A, Winterhalter T, Abate C, Sidorenco N, Hriţcu C, Maillard K and Spitters B. (2023). SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq. ACM Transactions on Programming Languages and Systems. 45:3. (1-61). Online publication date: 30-Sep-2023.

    https://doi.org/10.1145/3594735

  • Barbosa M, Barthe G, Grégoire B, Koutsos A and Strub P. (2023). Mechanized Proofs of Adversarial Complexity and Application to Universal Composability. ACM Transactions on Privacy and Security. 26:3. (1-34). Online publication date: 30-Aug-2023.

    https://doi.org/10.1145/3589962

  • Hvass B, Aranha D and Spitters B. (2023). High-Assurance Field Inversion for Curve-Based Cryptography 2023 IEEE 36th Computer Security Foundations Symposium (CSF). 10.1109/CSF57540.2023.00008. 979-8-3503-2192-0. (552-567).

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

  • Grégoire B, Léchenet J and Tassi E. Practical and Sound Equality Tests, Automatically: Deriving eqType Instances for Jasmin’s Data Types with Coq-Elpi. Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs. (167-181).

    https://doi.org/10.1145/3573105.3575683

  • Barbosa M, Dupressoir F, Grégoire B, Hülsing A, Meijers M and Strub P. (2023). Machine-Checked Security for $$\textrm{XMSS} $$ as in RFC 8391 and $$\mathrm {SPHINCS^{+}} $$. Advances in Cryptology – CRYPTO 2023. 10.1007/978-3-031-38554-4_14. (421-454).

    https://link.springer.com/10.1007/978-3-031-38554-4_14

  • Ammanaghatta Shivakumar B, Barthe G, Grégoire B, Laporte V and Priya S. Enforcing Fine-grained Constant-time Policies. Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security. (83-96).

    https://doi.org/10.1145/3548606.3560689

  • Hanson P, Winters B, Mercer E and Decker B. Verifying the SHA-3 Implementation from OpenSSL with the Software Analysis Workbench. Model Checking Software. (97-113).

    https://doi.org/10.1007/978-3-031-15077-7_6

  • Grilo M, Campos J, Ferreira J, Almeida J and Mendes A. (2022). Verified Password Generation from Password Composition Policies. Integrated Formal Methods. 10.1007/978-3-031-07727-2_15. (271-288).

    https://link.springer.com/10.1007/978-3-031-07727-2_15

  • Almeida J, Barbosa M, Correia M, Eldefrawy K, Graham-Lengrand S, Pacheco H and Pereira V. Machine-checked ZKP for NP relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head. Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security. (2587-2600).

    https://doi.org/10.1145/3460120.3484771

  • Barbosa M, Barthe G, Grégoire B, Koutsos A and Strub P. Mechanized Proofs of Adversarial Complexity and Application to Universal Composability. Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security. (2541-2563).

    https://doi.org/10.1145/3460120.3484548

  • Barthe G, Cauligi S, Grégoire B, Koutsos A, Liao K, Oliveira T, Priya S, Rezk T and Schwabe P. (2021). High-Assurance Cryptography in the Spectre Era 2021 IEEE Symposium on Security and Privacy (SP). 10.1109/SP40001.2021.00046. 978-1-7281-8934-5. (1884-1901).

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

  • 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/

  • Hohenberger S, Vusirikala S and Waters B. (2020). PPE Circuits: Formal Definition to Software Automation CCS '20: 2020 ACM SIGSAC Conference on Computer and Communications Security. 10.1145/3372297.3417230. 9781450370899. (391-408). Online publication date: 30-Oct-2020.

    https://dl.acm.org/doi/10.1145/3372297.3417230

  • Küennemann R and Nemati H. (2020). MAC-in-the-Box: Verifying a Minimalistic Hardware Design for MAC Computation. Computer Security – ESORICS 2020. 10.1007/978-3-030-59013-0_26. (525-545).

    http://link.springer.com/10.1007/978-3-030-59013-0_26