José Bacelar Almeida

According to our database, José Bacelar Almeida authored at least 40 papers between 2004 and 2024.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

2024

Formally verifying Kyber Episode V: Machine-checked IND-CCA security and correctness of ML-KEM in EasyCrypt.

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

IACR Cryptol. ePrint Arch., 2024

2023

Formally verifying Kyber Episode IV: Implementation correctness.

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

IACR Trans. Cryptogr. Hardw. Embed. Syst., 2023

Leakage-Free Probabilistic Jasmin Programs.

José Bacelar Almeida, Denis Firsov, Tiago Oliveira, Dominique Unruh

IACR Cryptol. ePrint Arch., 2023

Formally verifying Kyber Part I: Implementation Correctness.

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

IACR Cryptol. ePrint Arch., 2023

2022

A formal treatment of the role of verified compilers in secure computation.

José Carlos Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Hugo Pacheco, Vitor Pereira, Bernardo Portela

J. Log. Algebraic Methods Program., 2022

Verified Password Generation from Password Composition Policies.

Miguel Grilo, João Campos, João F. Ferreira, José Bacelar Almeida, Alexandra Mendes

Proceedings of the Integrated Formal Methods - 17th International Conference, 2022

2021

Machine-checked ZKP for NP-relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head.

José Bacelar Almeida, Manuel Barbosa, Manuel L. Correia, Karim Eldefrawy, Stéphane Graham-Lengrand, Hugo Pacheco, Vitor Pereira

IACR Cryptol. ePrint Arch., 2021

Towards Formal Verification of Password Generation Algorithms used in Password Managers.

Miguel Grilo, João F. Ferreira, José Bacelar Almeida

CoRR, 2021

Machine-checked ZKP for NP-relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head.

José Carlos Bacelar Almeida, Manuel Barbosa, Karim Eldefrawy, Stéphane Graham-Lengrand, Hugo Pacheco, Vitor Pereira

CoRR, 2021

2020

The Last Mile: High-Assurance and High-Speed Cryptographic Implementations.

José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Vincent Laporte, Tiago Oliveira, Pierre-Yves Strub

Proceedings of the 2020 IEEE Symposium on Security and Privacy, 2020

Certified Compilation for Cryptography: Extended x86 Instructions and Constant-Time Verification.

José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Vincent Laporte, Tiago Oliveira

Proceedings of the Progress in Cryptology - INDOCRYPT 2020, 2020

2019

A Machine-Checked Proof of Security for AWS Key Management Service.

José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Matthew Campagna, Ernie Cohen, Benjamin Grégoire, Vitor Pereira, Bernardo Portela, Pierre-Yves Strub, Serdar Tasiran

IACR Cryptol. ePrint Arch., 2019

Machine-Checked Proofs for Cryptographic Standards.

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

IACR Cryptol. ePrint Arch., 2019

Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3.

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

Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, 2019

2018

Teaching how to program using automated assessment and functional glossy games (experience report).

José Bacelar Almeida, Alcino Cunha, Nuno Macedo, Hugo Pacheco, José Proença

Proc. ACM Program. Lang., 2018

Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks.

José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Hugo Pacheco, Vitor Pereira, Bernardo Portela

IACR Cryptol. ePrint Arch., 2018

Some Applications of the Formalization of the Pumping Lemma for Context-Free Languages.

Marcus V. M. Ramos, José Carlos Bacelar Almeida, Nelma Moreira, Ruy J. G. B. de Queiroz

Proceedings of the 13th Workshop on Logical and Semantic Frameworks with Applications, 2018

2017

A Fast and Verified Software Stack for Secure Function Evaluation.

José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Vitor Pereira

IACR Cryptol. ePrint Arch., 2017

Jasmin: High-Assurance and High-Speed Cryptography.

José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Arthur Blot, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Hugo Pacheco, Benedikt Schmidt, Pierre-Yves Strub

Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, 2017

2016

Formalization of the pumping lemma for context-free languages.

Marcus Vinícius Midena Ramos, José Carlos Bacelar Almeida, Nelma Moreira, Ruy José Guerra Barretto de Queiroz

J. Formaliz. Reason., 2016

A Tool-Chain for High-Assurance Cryptographic Software.

José Bacelar Almeida, Manuel Barbosa, Hugo Pacheco, Vitor Pereira

ERCIM News, 2016

On the Formalization of Some Results of Context-Free Language Theory.

Marcus Vinícius Midena Ramos, Ruy J. G. B. de Queiroz, Nelma Moreira, José Carlos Bacelar Almeida

Proceedings of the Logic, Language, Information, and Computation, 2016

Verifying Constant-Time Implementations.

José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, Michael Emmi

Proceedings of the 25th USENIX Security Symposium, 2016

2015

Verifiable side-channel security of cryptographic implementations: constant-time MEE-CBC.

José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir

IACR Cryptol. ePrint Arch., 2015

Formalization of context-free language theory.

Marcus V. M. Ramos, Ruy J. G. B. de Queiroz, Nelma Moreira, José Carlos Bacelar Almeida

CoRR, 2015

2014

CAOVerif: An open-source deductive verification platform for cryptographic software implementations.

José Bacelar Almeida, Manuel Barbosa, Jean-Christophe Filliâtre, Jorge Sousa Pinto, Bárbara Vieira

Sci. Comput. Program., 2014

Verified Implementations for Secure and Verifiable Computation.

José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Guillaume Davy, François Dupressoir, Benjamin Grégoire, Pierre-Yves Strub

IACR Cryptol. ePrint Arch., 2014

2013

Formal verification of side-channel countermeasures using self-composition.

José Bacelar Almeida, Manuel Barbosa, Jorge Sousa Pinto, Bárbara Vieira

Sci. Comput. Program., 2013

Certified computer-aided cryptography: efficient provably secure machine code from high-level implementations.

José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir

IACR Cryptol. ePrint Arch., 2013

2012

Full Proof Cryptography: Verifiable Compilation of Efficient Zero-Knowledge Protocols.

José Bacelar Almeida, Manuel Barbosa, Endre Bangerter, Gilles Barthe, Stephan Krenn, Santiago Zanella Béguelin

IACR Cryptol. ePrint Arch., 2012

2011

Rigorous Software Development - An Introduction to Program Verification.

José Bacelar Almeida, Maria João Frade, Jorge Sousa Pinto, Simão Melo de Sousa

Undergraduate Topics in Computer Science, Springer, ISBN: 978-0-85729-018-2, 2011

2010

Deductive verification of cryptographic software.

José Bacelar Almeida, Manuel Barbosa, Jorge Sousa Pinto, Bárbara Vieira

Innov. Syst. Softw. Eng., 2010

A Certifying Compiler for Zero-Knowledge Proofs of Knowledge Based on Sigma-Protocols.

José Bacelar Almeida, Endre Bangerter, Manuel Barbosa, Stephan Krenn, Ahmad-Reza Sadeghi, Thomas Schneider

IACR Cryptol. ePrint Arch., 2010

Partial Derivative Automata Formalized in Coq.

José Bacelar Almeida, Nelma Moreira, David Pereira, Simão Melo de Sousa

Proceedings of the Implementation and Application of Automata, 2010

2009

Verifying Cryptographic Software Correctness with Respect to Reference Implementations.

José Bacelar Almeida, Manuel Barbosa, Jorge Sousa Pinto, Bárbara Vieira

Proceedings of the Formal Methods for Industrial Critical Systems, 2009

2008

Deriving Sorting Algorithms

José Bacelar Almeida, Jorge Sousa Pinto

CoRR, 2008

2007

A Tool for Programming with Interaction Nets.

José Bacelar Almeida, Jorge Sousa Pinto, Miguel Vilaça

Proceedings of the Eighth International Workshop on Rule Based Programming, 2007

Token-passing Nets for Functional Languages.

José Bacelar Almeida, Jorge Sousa Pinto, Miguel Vilaça

Proceedings of the 7th International Workshop on Reduction Strategies in Rewriting and Programming, 2007

2006

A Local Graph-rewriting System for Deciding Equality in Sum-product Theories.

José Bacelar Almeida, Jorge Sousa Pinto, Miguel Vilaça

Proceedings of the Third International Workshop on Term Graph Rewriting, 2006

2004

Bounded Version Vectors.

José Bacelar Almeida, Paulo Sérgio Almeida, Carlos Baquero

Proceedings of the Distributed Computing, 18th International Conference, 2004