| A fast and verified software stack for secure function evaluation JB Almeida, M Barbosa, G Barthe, F Dupressoir, B Grégoire, V Laporte, ... Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications …, 2017 | 37 | 2017 |
| A machine-checked proof of security for AWS key management service JB Almeida, M Barbosa, G Barthe, M Campagna, E Cohen, B Gregoire, ... Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications …, 2019 | 31 | 2019 |
| Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks JB Almeida, M Barbosa, G Barthe, H Pacheco, V Pereira, B Portela 2018 IEEE 31st Computer Security Foundations Symposium (CSF), 132-146, 2018 | 16 | 2018 |
| Machine-checked ZKP for NP relations: Formally verified security proofs and implementations of MPC-in-the-head JB Almeida, M Barbosa, ML Correia, K Eldefrawy, S Graham-Lengrand, ... Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications …, 2021 | 15 | 2021 |
| A high-assurance evaluator for machine-checked secure multiparty computation K Eldefrawy, V Pereira Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications …, 2019 | 10 | 2019 |
| A formal treatment of the role of verified compilers in secure computation JCB Almeida, M Barbosa, G Barthe, H Pacheco, V Pereira, B Portela Journal of Logical and Algebraic Methods in Programming 125, 100736, 2022 | 4 | 2022 |
| Boosting the Performance of High-Assurance Cryptography: Parallel Execution and Optimizing Memory Access in Formally-Verified Line-Point Zero-Knowledge S Dittmer, K Eldefrawy, S Graham-Lengrand, S Lu, R Ostrovsky, V Pereira Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications …, 2023 | 2 | 2023 |
| Machine-checked ZKP for NP-relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head JC Bacelar Almeida, M Barbosa, K Eldefrawy, S Graham-Lengrand, ... arXiv e-prints, arXiv: 2104.05516, 2021 | | 2021 |
| A High-Assurance, Automatically-Synthesized, Evaluator for Machine-Checked (Proactively) Secure Multi-Party Computation. K Eldefrawy, V Pereira IACR Cryptol. ePrint Arch. 2019, 922, 2019 | | 2019 |
| Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks HP Pacheco, BL Portela, VP Pereira, JB Almeida, M Barbosa, G Barthe | | 2018 |
| A Tool-Chain for High-Assurance Cryptographic Software JB Almeida, M Barbosa, HP Pacheco, V Pereira | | 2016 |
| A deductive verification tool for cryptographic software VMP Pereira | | 2015 |
Manuel BarbosaUniversidade do Porto (FCUP) and INESC TECAdresse e-mail validée de fc.up.pt