José Bacelar Almeida

Publication Activity (10 Years)

Years Active: 2004-2024
Publications (10 Years): 25

Top Topics

Top Venues

IACR Cryptol. ePrint Arch.

IEEE Symposium on Security and Privacy

Publications

José Bacelar Almeida, Santiago Arranz Olmos, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Cameron Low, Tiago Oliveira, Hugo Pacheco, Miguel Quaresma, Peter Schwabe, Pierre-Yves Strub
Formally verifying Kyber Episode V: Machine-checked IND-CCA security and correctness of ML-KEM in EasyCrypt. IACR Cryptol. ePrint Arch. 2024 (2024)
José Bacelar Almeida, Santiago Arranz Olmos, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Cameron Low, Tiago Oliveira, Hugo Pacheco, Miguel Quaresma, Peter Schwabe, Pierre-Yves Strub
Formally Verifying Kyber - Episode V: Machine-Checked IND-CCA Security and Correctness of ML-KEM in EasyCrypt. CRYPTO (2) (2024)
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Tiago Oliveira, Hugo Pacheco, Miguel Quaresma, Peter Schwabe, Antoine Séré, Pierre-Yves Strub
Formally verifying Kyber Part I: Implementation Correctness. IACR Cryptol. ePrint Arch. 2023 (2023)
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Tiago Oliveira, Hugo Pacheco, Miguel Quaresma, Peter Schwabe, Antoine Séré, Pierre-Yves Strub
Formally verifying Kyber Episode IV: Implementation correctness. IACR Trans. Cryptogr. Hardw. Embed. Syst. 2023 (3) (2023)
José Bacelar Almeida, Denis Firsov, Tiago Oliveira, Dominique Unruh
Leakage-Free Probabilistic Jasmin Programs. IACR Cryptol. ePrint Arch. 2023 (2023)
Miguel Grilo, João Campos, João F. Ferreira, José Bacelar Almeida, Alexandra Mendes
Verified Password Generation from Password Composition Policies. IFM (2022)
Miguel Grilo, João F. Ferreira, José Bacelar Almeida
Towards Formal Verification of Password Generation Algorithms used in Password Managers. CoRR (2021)
José Bacelar Almeida, Manuel Barbosa, Manuel L. Correia, Karim Eldefrawy, Stéphane Graham-Lengrand, Hugo Pacheco, Vitor Pereira
Machine-checked ZKP for NP relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head. CCS (2021)
José Bacelar Almeida, Manuel Barbosa, Manuel L. Correia, Karim Eldefrawy, Stéphane Graham-Lengrand, Hugo Pacheco, Vitor Pereira
Machine-checked ZKP for NP-relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head. IACR Cryptol. ePrint Arch. 2021 (2021)
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Vincent Laporte, Tiago Oliveira
Certified Compilation for Cryptography: Extended x86 Instructions and Constant-Time Verification. INDOCRYPT (2020)
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Vincent Laporte, Tiago Oliveira, Pierre-Yves Strub
The Last Mile: High-Assurance and High-Speed Cryptographic Implementations. IEEE Symposium on Security and Privacy (2020)
José Bacelar Almeida, Cécile Baritel-Ruet, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Alley Stoughton, Pierre-Yves Strub
Machine-Checked Proofs for Cryptographic Standards. IACR Cryptol. ePrint Arch. 2019 (2019)
José Bacelar Almeida, Cécile Baritel-Ruet, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Alley Stoughton, Pierre-Yves Strub
Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3. CCS (2019)
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Matthew Campagna, Ernie Cohen, Benjamin Grégoire, Vitor Pereira, Bernardo Portela, Pierre-Yves Strub, Serdar Tasiran
A Machine-Checked Proof of Security for AWS Key Management Service. IACR Cryptol. ePrint Arch. 2019 (2019)
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Matthew Campagna, Ernie Cohen, Benjamin Grégoire, Vitor Pereira, Bernardo Portela, Pierre-Yves Strub, Serdar Tasiran
A Machine-Checked Proof of Security for AWS Key Management Service. CCS (2019)
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Vincent Laporte, Tiago Oliveira, Pierre-Yves Strub
The Last Mile: High-Assurance and High-Speed Cryptographic Implementations. CoRR (2019)
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Hugo Pacheco, Vitor Pereira, Bernardo Portela
Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks. IACR Cryptol. ePrint Arch. 2018 (2018)
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Hugo Pacheco, Vitor Pereira, Bernardo Portela
Enforcing Ideal-World Leakage Bounds in Real-World Secret Sharing MPC Frameworks. CSF (2018)
José Bacelar Almeida, Alcino Cunha, Nuno Macedo, Hugo Pacheco, José Proença
Teaching how to program using automated assessment and functional glossy games (experience report). Proc. ACM Program. Lang. 2 (ICFP) (2018)
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Arthur Blot, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Hugo Pacheco, Benedikt Schmidt, Pierre-Yves Strub
Jasmin: High-Assurance and High-Speed Cryptography. CCS (2017)
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Vitor Pereira
A Fast and Verified Software Stack for Secure Function Evaluation. IACR Cryptol. ePrint Arch. 2017 (2017)
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Vitor Pereira
A Fast and Verified Software Stack for Secure Function Evaluation. CCS (2017)
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, Michael Emmi
Verifying Constant-Time Implementations. USENIX Security Symposium (2016)
José Bacelar Almeida, Manuel Barbosa, Hugo Pacheco, Vitor Pereira
A Tool-Chain for High-Assurance Cryptographic Software. ERCIM News 2016 (106) (2016)
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir
Verifiable Side-Channel Security of Cryptographic Implementations: Constant-Time MEE-CBC. FSE (2016)
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir
Verifiable side-channel security of cryptographic implementations: constant-time MEE-CBC. IACR Cryptol. ePrint Arch. 2015 (2015)
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Guillaume Davy, François Dupressoir, Benjamin Grégoire, Pierre-Yves Strub
Verified Implementations for Secure and Verifiable Computation. IACR Cryptol. ePrint Arch. 2014 (2014)
José Bacelar Almeida, Manuel Barbosa, Jean-Christophe Filliâtre, Jorge Sousa Pinto, Bárbara Vieira
CAOVerif: An open-source deductive verification platform for cryptographic software implementations. Sci. Comput. Program. 91 (2014)
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir
Certified computer-aided cryptography: efficient provably secure machine code from high-level implementations. CCS (2013)
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir
Certified computer-aided cryptography: efficient provably secure machine code from high-level implementations. IACR Cryptol. ePrint Arch. 2013 (2013)
José Bacelar Almeida, Manuel Barbosa, Jorge Sousa Pinto, Bárbara Vieira
Formal verification of side-channel countermeasures using self-composition. Sci. Comput. Program. 78 (7) (2013)
José Bacelar Almeida, Manuel Barbosa, Endre Bangerter, Gilles Barthe, Stephan Krenn, Santiago Zanella Béguelin
Full Proof Cryptography: Verifiable Compilation of Efficient Zero-Knowledge Protocols. IACR Cryptol. ePrint Arch. 2012 (2012)
José Bacelar Almeida, Manuel Barbosa, Endre Bangerter, Gilles Barthe, Stephan Krenn, Santiago Zanella Béguelin
Full proof cryptography: verifiable compilation of efficient zero-knowledge protocols. CCS (2012)
José Bacelar Almeida, Manuel Barbosa, Jorge Sousa Pinto, Bárbara Vieira
Deductive verification of cryptographic software. Innov. Syst. Softw. Eng. 6 (3) (2010)
José Bacelar Almeida, Endre Bangerter, Manuel Barbosa, Stephan Krenn, Ahmad-Reza Sadeghi, Thomas Schneider
A Certifying Compiler for Zero-Knowledge Proofs of Knowledge Based on Sigma-Protocols. IACR Cryptol. ePrint Arch. 2010 (2010)
José Bacelar Almeida, Nelma Moreira, David Pereira, Simão Melo de Sousa
Partial Derivative Automata Formalized in Coq. CIAA (2010)
José Bacelar Almeida, Endre Bangerter, Manuel Barbosa, Stephan Krenn, Ahmad-Reza Sadeghi, Thomas Schneider
A Certifying Compiler for Zero-Knowledge Proofs of Knowledge Based on Sigma-Protocols. ESORICS (2010)
Manuel Barbosa, José Bacelar Almeida, Jorge Sousa Pinto, Bárbara Vieira
Deductive Verification of Cryptographic Software. NASA Formal Methods (2009)
José Bacelar Almeida, Manuel Barbosa, Jorge Sousa Pinto, Bárbara Vieira
Verifying Cryptographic Software Correctness with Respect to Reference Implementations. FMICS (2009)
José Bacelar Almeida, Jorge Sousa Pinto, Miguel Vilaça
A Tool for Programming with Interaction Nets. Electron. Notes Theor. Comput. Sci. 219 (2008)
José Bacelar Almeida, Jorge Sousa Pinto
Deriving Sorting Algorithms CoRR (2008)
José Bacelar Almeida, Jorge Sousa Pinto, Miguel Vilaça
Token-passing Nets for Functional Languages. Electron. Notes Theor. Comput. Sci. 204 (2008)
José Bacelar Almeida, Jorge Sousa Pinto, Miguel Vilaça
A Local Graph-rewriting System for Deciding Equality in Sum-product Theories. Electron. Notes Theor. Comput. Sci. 176 (1) (2007)
José Bacelar Almeida, Paulo Sérgio Almeida, Carlos Baquero
Bounded Version Vectors. DISC (2004)