Research output per year
Research output 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
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
-
Completing the Chain: Verified Implementations of Hash-Based Signatures and Their Security
Barbosa, M., Dupressoir, F., Fernandes, R., Hülsing, A., Meijers, M. & Strub, P. Y., 17 Jul 2026, In: IACR Transactions on Cryptographic Hardware and Embedded Systems. 2026, 3, p. 958-981 24 p.Research output: Contribution to journal › Article › peer-review
Open Access -
Functional Correctness of an Optimized Modular Inversion Algorithm
Mahboubi, A., Melquiond, G., Strub, P. Y. & Parada, T. V., 16 Jul 2026, 17th International Conference on Interactive Theorem Proving, ITP 2026. Komendantskaya, E., Komendantskaya, E. & Nipkow, T. (eds.). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 9. (Leibniz International Proceedings in Informatics, LIPIcs; vol. 382).Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review
-
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 Access4 Citations (Scopus) -
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 Access1 Citation (Scopus) -
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 Access1 Citation (Scopus) -
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 Access1 Citation (Scopus) -
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 Access17 Citations (Scopus) -
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 Access8 Citations (Scopus) -
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 Access3 Citations (Scopus)