No photo of Pierre-Yves Strub

View Scopus Profile

Pierre-Yves Strub

20072025

Research activity per year

Fingerprint

Dive into the research topics where Pierre-Yves Strub is active. These topic labels come from the works of this person. Together they form a unique fingerprint.
  • 1 Similar Profiles
View full fingerprint

Collaborations and top research areas from the last five years

Recent external collaboration on country/territory level. Dive into details by clicking on the dots or
Explore network further

  • A Tight Security Proof for SPHINCS+, Formally Verified

    Barbosa, M., Dupressoir, F., Hülsing, A., Meijers, M. & Strub, P. Y., 1 Jan 2025, Advances in Cryptology – ASIACRYPT 2024 - 30th International Conference on the Theory and Application of Cryptology and Information Security, Proceedings. Chung, K.-M. & Sasaki, Y. (eds.). Springer Science and Business Media Deutschland GmbH, p. 35-67 33 p. (Lecture Notes in Computer Science; vol. 15487 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    Open Access

  • Faster Verification of Faster Implementations: Combining Deductive and Circuit-Based Reasoning in EasyCrypt

    Almeida, J. B., Delerue Marinho Alves, G. X., Barbosa, M., Barthe, G., Esquível, L., Hwang, V., Oliveira, T., Pacheco, H., Schwabe, P. & Strub, P. Y., 1 Jan 2025, Proceedings - 46th IEEE Symposium on Security and Privacy, SP 2025. Blanton, M., Enck, W. & Nita-Rotaru, C. (eds.). Institute of Electrical and Electronics Engineers Inc., p. 3820-3838 19 p. (Proceedings - IEEE Symposium on Security and Privacy).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

  • Formally Verified Correctness Bounds for Lattice-Based Cryptography

    Barbosa, M., Kannwischer, M. J., Lim, T. H., Schwabe, P. & Strub, P. Y., 22 Nov 2025, CCS 2025 - Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security. Association for Computing Machinery, Inc, p. 156-169 14 p. (CCS 2025 - Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    Open Access

  • Jazzline: Composable CryptoLine Functional Correctness Proofs for Jasmin Programs

    Almeida, J. B., Barbosa, M., Barthe, G., Blatter, L., Delerue, G., Duarte, J. D., Gregoire, B., Oliveira, T., Quaresma, M., Strub, P. Y., Tsai, M. H., Wang, B. Y. & Yang, B. Y., 22 Nov 2025, CCS 2025 - Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security. Association for Computing Machinery, Inc, p. 1409-1423 15 p. (CCS 2025 - Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    Open Access

  • CV2EC: Getting the Best of Both Worlds

    Blanchet, B., Boutry, P., Doczkal, C., Gregoire, B. & Strub, P. Y., 1 Jan 2024, Proceedings - 2024 IEEE 37th Computer Security Foundations Symposium, CSF 2024. IEEE Computer Society, p. 279-294 16 p. (Proceedings - IEEE Computer Security Foundations Symposium).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    Open Access

  • Formally Verifying Kyber: Episode V: Machine-Checked IND-CCA Security and Correctness of ML-KEM in EasyCrypt

    Almeida, J. B., Arranz Olmos, S., Barbosa, M., Barthe, G., Dupressoir, F., Grégoire, B., Laporte, V., Léchenet, J. C., Low, C., Oliveira, T., Pacheco, H., Quaresma, M., Schwabe, P. & Strub, P. Y., 1 Jan 2024, Advances in Cryptology – CRYPTO 2024 - 44th Annual International Cryptology Conference, Proceedings. Reyzin, L. & Stebila, D. (eds.). Springer Science and Business Media Deutschland GmbH, p. 384-421 38 p. (Lecture Notes in Computer Science; vol. 14921 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    Open Access

  • High-Performance NTT Hardware Accelerator to Support ML-KEM and ML-DSA

    Kundi, D. E. S., Bermudo Mera, J. M., Strub, P. Y. & Hutter, M., 19 Nov 2024, ASHES 2024 - Proceedings of the 2024 Workshop on Attacks and Solutions in Hardware Security, Co-Located with: CCS 2024. Association for Computing Machinery, Inc, p. 100-105 6 p. (ASHES 2024 - Proceedings of the 2024 Workshop on Attacks and Solutions in Hardware Security, Co-Located with: CCS 2024).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    Open Access

  • A Formal Disproof of Hirsch Conjecture

    Allamigeon, X., Canu, Q. & Strub, P. Y., 11 Jan 2023, CPP 2023 - Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2023. Krebbers, R., Traytel, D., Pientka, B. & Zdancewic, S. (eds.). Association for Computing Machinery, Inc, p. 17-29 13 p. (CPP 2023 - Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2023).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

    Open Access

  • CoqQ: Foundational Verification of Quantum Programs

    Zhou, L., Barthe, G., Strub, P. Y., Liu, J. & Ying, M., 9 Jan 2023, In: Proceedings of the ACM on Programming Languages. 7, p. 833-865 33 p.

    Research output: Contribution to journal › Article › peer-review

    Open Access

  • Formally verifying Kyber Episode IV: Implementation correctness

    Almeida, J. B., Barbosa, M., Barthe, G., Grégoire, B., Laporte, V., Léchenet, J. C., Oliveira, T., Pacheco, H., Quaresma, M., Schwabe, P., Séré, A. & Strub, P. Y., 9 Jun 2023, In: IACR Transactions on Cryptographic Hardware and Embedded Systems. 2023, 3, p. 164-193 30 p.

    Research output: Contribution to journal › Article › peer-review

    Open Access
View all 75 research outputs