| A Tight Security Proof for , Formally Verified M Barbosa, F Dupressoir, A Hülsing, M Meijers, PY Strub Cryptology ePrint Archive, 2024 | | 2024 |
| Formally verifying Kyber Episode V: Machine-checked IND-CCA security and correctness of ML-KEM in EasyCrypt JB Almeida, SA Olmos, M Barbosa, G Barthe, F Dupressoir, B Grégoire, ... Cryptology ePrint Archive, 2024 | 1 | 2024 |
| Formally verifying Kyber JB Almeida, SA Olmos, M Barbosa, G Barthe, F Dupressoir, B Grégoire, ... | 14 | 2024 |
| CV2EC: Getting the Best of Both Worlds B Blanchet, P Boutry, C Doczkal, B Grégoire, PY Strub | | 2023 |
| Machine-Checked Security for as in RFC 8391 and M Barbosa, F Dupressoir, B Grégoire, A Hülsing, M Meijers, PY Strub Annual International Cryptology Conference, 421-454, 2023 | 4 | 2023 |
| A formal disproof of hirsch conjecture X Allamigeon, Q Canu, PY Strub Proceedings of the 12th ACM SIGPLAN International Conference on Certified …, 2023 | 3 | 2023 |
| Coqq: Foundational verification of quantum programs L Zhou, G Barthe, PY Strub, J Liu, M Ying Proceedings of the ACM on Programming Languages 7 (POPL), 833-865, 2023 | 26 | 2023 |
| Design patterns of hierarchies for order structures X Allamigeon, Q Canu, C Cohen, K Sakaguchi, PY Strub | 5 | 2023 |
| Formal verification of Saber’s public-key encryption scheme in EasyCrypt A Hülsing, M Meijers, PY Strub Annual International Cryptology Conference, 622-653, 2022 | 10 | 2022 |
| Actema: une interface graphique et gestuelle pour preuves formelles (démonstration) P Donato, PY Strub, B Werner 33èmes Journées Francophones des Langages Applicatifs, 267-268, 2022 | | 2022 |
| Formalizing the face lattice of polyhedra X Allamigeon, RD Katz, PY Strub Logical Methods in Computer Science 18, 2022 | 5 | 2022 |
| A Formalization of the Proof of Correctness of a Number-Theoretic Transform in the Context of the Hakyber Cryptographic Primitive A Séré, PY Strub Journées 2022 du GT” Méthodes Formelles pour la Sécurité”, GdR Sécurité …, 2022 | | 2022 |
| A drag-and-drop proof tactic P Donato, PY Strub, B Werner Proceedings of the 11th ACM SIGPLAN International Conference on Certified …, 2022 | 14 | 2022 |
| EasyPQC: Verifying post-quantum cryptography M Barbosa, G Barthe, X Fan, B Grégoire, SH Hung, J Katz, PY Strub, X Wu, ... Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications …, 2021 | 24 | 2021 |
| Mechanized proofs of adversarial complexity and application to universal composability M Barbosa, G Barthe, B Grégoire, A Koutsos, PY Strub Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications …, 2021 | 23 | 2021 |
| Unsolvability of the quintic formalized in dependent type theory S Bernard, C Cohen, A Mahboubi, PY Strub ITP 2021-12th International Conference on Interactive Theorem Proving, 2021 | 5 | 2021 |
| 12th International Conference on Interactive Theorem Proving (ITP 2021) MO Myreen, N Polikarpova, A Popescu, T Bauereiss, P Lammich, ... Schloss Dagstuhl-Leibniz-Zentrum für Informatik GmbH, 2021 | | 2021 |
| Intuitionistic Subformula Linking B Werner, PY Strub | | 2020 |
| The last mile: High-assurance and high-speed cryptographic implementations JB Almeida, M Barbosa, G Barthe, B Grégoire, A Koutsos, V Laporte, ... 2020 IEEE Symposium on Security and Privacy (SP), 965-982, 2020 | 88 | 2020 |
| Improved parallel mask refreshing algorithms: generic solutions with parametrized non-interference and automated optimizations G Barthe, S Belaïd, F Dupressoir, PA Fouque, B Grégoire, FX Standaert, ... Journal of Cryptographic Engineering 10, 17-26, 2020 | 24 | 2020 |
Cédric FournetMicrosoft Research在 microsoft.com 的电子邮件经过验证
