| Jasmin: High-assurance and high-speed cryptography JB Almeida, M Barbosa, G Barthe, A Blot, B Grégoire, V Laporte, ... Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications …, 2017 | 198 | 2017 |
| 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 | 99 | 2020 |
| Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3 JB Almeida, C Baritel-Ruet, M Barbosa, G Barthe, F Dupressoir, ... Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications …, 2019 | 62 | 2019 |
| High-assurance cryptography in the spectre era G Barthe, S Cauligi, B Grégoire, A Koutsos, K Liao, T Oliveira, S Priya, ... 2021 IEEE Symposium on Security and Privacy (SP), 1884-1901, 2021 | 49 | 2021 |
| A practical framework for privacy-preserving nosql databases R Macedo, J Paulo, R Pontes, B Portela, T Oliveira, M Matos, R Oliveira 2017 IEEE 36th Symposium on Reliable Distributed Systems (SRDS), 11-20, 2017 | 31 | 2017 |
| Typing high-speed cryptography against spectre v1 BA Shivakumar, G Barthe, B Grégoire, V Laporte, T Oliveira, S Priya, ... 2023 IEEE Symposium on Security and Privacy (SP), 1094-1111, 2023 | 27 | 2023 |
| Formally verifying Kyber Episode IV: Implementation Correctness JB Almeida, M Barbosa, G Barthe, B Grégoire, V Laporte, JC Léchenet, ... Cryptology ePrint Archive, 2023 | 21* | 2023 |
| Boolean searchable symmetric encryption with filters on trusted hardware B Ferreira, B Portela, T Oliveira, G Borges, H Domingos, J Leitão IEEE Transactions on Dependable and Secure Computing 19 (2), 1307-1319, 2020 | 20 | 2020 |
| Bisen: Efficient boolean searchable symmetric encryption with verifiability and minimal leakage B Ferreira, B Portela, T Oliveira, G Borges, H Domingos, J Leitão 2019 38th Symposium on Reliable Distributed Systems (SRDS), 103-10309, 2019 | 9 | 2019 |
| Certified compilation for cryptography: Extended x86 instructions and constant-time verification JB Almeida, M Barbosa, G Barthe, V Laporte, T Oliveira Progress in Cryptology–INDOCRYPT 2020: 21st International Conference on …, 2020 | 6 | 2020 |
| Formally Verifying Kyber: Episode V: Machine-Checked IND-CCA Security and Correctness of ML-KEM in EasyCrypt JB Almeida, S Arranz Olmos, M Barbosa, G Barthe, F Dupressoir, ... Annual International Cryptology Conference, 384-421, 2024 | 3 | 2024 |
| Schnorr protocol in Jasmin JB Almeida, D Firsov, T Oliveira, D Unruh Cryptology ePrint Archive, 2023 | 3* | 2023 |
| Are Deep Learning Methods Ready for Prime Time in Fingerprints Minutiae Extraction? A Rebelo, T Oliveira, ME Correia, JS Cardoso Iberoamerican Congress on Pattern Recognition, 628-636, 2018 | 3 | 2018 |
| Protecting cryptographic code against Spectre-RSB (and, in fact, all known Spectre variants) SA Olmos, G Barthe, C Chuengsatiansup, B Grégoire, V Laporte, ... | 2 | 2024 |
| High-assurance zeroization SA Olmos, G Barthe, R Gonzalez, B Grégoire, V Laporte, JC Léchenet, ... IACR Transactions on Cryptographic Hardware and Embedded Systems 2024 (1 …, 2024 | 2 | 2024 |
| Leakage-Free Probabilistic Jasmin Programs JB Almeida, D Firsov, T Oliveira, D Unruh Cryptology ePrint Archive, 2023 | 1 | 2023 |
| High-speed and High-assurance Cryptographic Software TFA Oliveira | 1 | 2022 |
| Verificação de software criptográfico de elevado desempenho TFA Oliveira PQDT-Global, 2012 | 1 | 2012 |
| Formal Verification Challenges on High-Speed Cryptographic Implementations M Quaresma, T Oliveira Journées 2022 du GT” Méthodes Formelles pour la Sécurité”, GdR Sécurité …, 2022 | | 2022 |
Gilles BartheMPI-SP and IMDEA Software InstituteVerified email at mpi-sp.org
