Vitor Pereira

18 papers A* 5A 1Journal 11
YearRankTypeTitle / Venue / Authors
2025 J jnl
Who Verifies the Verifiers? Lessons Learned From Formally Verified Line-Point Zero-Knowledge.
IACR Cryptol. ePrint Arch.
Sabine Oechsner, Vitor Pereira, Peter Scholl
2025 J jnl
Who Verifies the Verifiers?: Lessons Learned From Formally Verified Line-Point Zero-Knowledge.
IACR Commun. Cryptol.
Sabine Oechsner, Vitor Pereira, Peter Scholl
2023 A* conf
Boosting the Performance of High-Assurance Cryptography: Parallel Execution and Optimizing Memory Access in Formally-Verified Line-Point Zero-Knowledge.
CCS
Samuel Dittmer, Karim Eldefrawy, Stéphane Graham-Lengrand, Steve Lu, Rafail Ostrovsky, Vitor Pereira
2023 J jnl
Boosting the Performance of High-Assurance Cryptography: Parallel Execution and Optimizing Memory Access in Formally-Verified Line-Point Zero-Knowledge.
IACR Cryptol. ePrint Arch.
Samuel Dittmer, Karim Eldefrawy, Stéphane Graham-Lengrand, Steve Lu, Rafail Ostrovsky, Vitor Pereira
2022 J jnl
A formal treatment of the role of verified compilers in secure computation.
J. Log. Algebraic Methods Program.
José Carlos Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Hugo Pacheco, Vitor Pereira, Bernardo Portela
2021 A* conf
Machine-checked ZKP for NP relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head.
CCS
José Bacelar Almeida, Manuel Barbosa, Manuel L. Correia, Karim Eldefrawy, Stéphane Graham-Lengrand, Hugo Pacheco, Vitor Pereira
2021 J jnl
Machine-checked ZKP for NP-relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head.
CoRR
José Carlos Bacelar Almeida, Manuel Barbosa, Karim Eldefrawy, Stéphane Graham-Lengrand, Hugo Pacheco, Vitor Pereira
2021 J jnl
Machine-checked ZKP for NP-relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head.
IACR Cryptol. ePrint Arch.
José Bacelar Almeida, Manuel Barbosa, Manuel L. Correia, Karim Eldefrawy, Stéphane Graham-Lengrand, Hugo Pacheco, Vitor Pereira
2020 — —
Integrated Verification of Cryptographic Security Proofs and Implementations
Vitor Pereira
2019 A* conf
A High-Assurance Evaluator for Machine-Checked Secure Multiparty Computation.
CCS
Karim Eldefrawy, Vitor Pereira
2019 J jnl
A High-Assurance, Automatically-Synthesized, Evaluator for Machine-Checked (Proactively) Secure Multi-Party Computation.
IACR Cryptol. ePrint Arch.
Karim Eldefrawy, Vitor Pereira
2019 A* conf
A Machine-Checked Proof of Security for AWS Key Management Service.
CCS
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Matthew Campagna, Ernie Cohen, Benjamin Grégoire, Vitor Pereira, Bernardo Portela, Pierre-Yves Strub, Serdar Tasiran
2019 J jnl
A Machine-Checked Proof of Security for AWS Key Management Service.
IACR Cryptol. ePrint Arch.
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Matthew Campagna, Ernie Cohen, Benjamin Grégoire, Vitor Pereira, Bernardo Portela, Pierre-Yves Strub, Serdar Tasiran
2018 A conf
Enforcing Ideal-World Leakage Bounds in Real-World Secret Sharing MPC Frameworks.
CSF
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Hugo Pacheco, Vitor Pereira, Bernardo Portela
2018 J jnl
Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks.
IACR Cryptol. ePrint Arch.
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Hugo Pacheco, Vitor Pereira, Bernardo Portela
2017 A* conf
A Fast and Verified Software Stack for Secure Function Evaluation.
CCS
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Vitor Pereira
2017 J jnl
A Fast and Verified Software Stack for Secure Function Evaluation.
IACR Cryptol. ePrint Arch.
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Vitor Pereira
2016 J jnl
A Tool-Chain for High-Assurance Cryptographic Software.
ERCIM News
José Bacelar Almeida, Manuel Barbosa, Hugo Pacheco, Vitor Pereira