Cookies
O website necessita de alguns cookies e outros recursos semelhantes para funcionar. Caso o permita, o INESC TEC irá utilizar cookies para recolher dados sobre as suas visitas, contribuindo, assim, para estatísticas agregadas que permitem melhorar o nosso serviço. Ver mais
Aceitar Rejeitar
  • Menu
Tópicos
de interesse
Detalhes

Detalhes

  • Nome

    José Bacelar Almeida
  • Cargo

    Investigador Sénior
  • Desde

    01 novembro 2011
003
Publicações

2024

Formally Verifying Kyber Episode V: Machine-Checked IND-CCA Security and Correctness of ML-KEM in EasyCrypt

Autores
Almeida, JB; Olmos, SA; Barbosa, M; Barthe, G; Dupressoir, F; Grégoire, B; Laporte, V; Lechenet, JC; Low, C; Oliveira, T; Pacheco, H; Quaresma, M; Schwabe, P; Strub, PY;

Publicação
ADVANCES IN CRYPTOLOGY - CRYPTO 2024, PT II

Abstract
We present a formally verified proof of the correctness and IND-CCA security of ML-KEM, the Kyber-based Key Encapsulation Mechanism (KEM) undergoing standardization by NIST. The proof is machine-checked in EasyCrypt and it includes: 1) A formalization of the correctness (decryption failure probability) and IND-CPA security of the Kyber base public-key encryption scheme, following Bos et al. at Euro S&P 2018; 2) A formalization of the relevant variant of the Fujisaki-Okamoto transform in the Random Oracle Model (ROM), which follows closely (but not exactly) Hofheinz, Hovelmanns and Kiltz at TCC 2017; 3) A proof that the IND-CCA security of the ML-KEM specification and its correctness as a KEM follows from the previous results; 4) Two formally verified implementations of ML-KEM written in Jasmin that are provably constant-time, functionally equivalent to the ML-KEM specification and, for this reason, inherit the provable security guarantees established in the previous points. The top-level theorems give self-contained concrete bounds for the correctness and security of ML-KEM down to (a variant of) Module-LWE. We discuss how they are built modularly by leveraging various EasyCrypt features.

2023

Formally verifying Kyber Episode IV: Implementation correctness

Autores
Almeida, JB; Barbosa, M; Barthe, G; Grégoire, B; Laporte, V; Léchenet, JC; Oliveira, T; Pacheco, H; Quaresma, M; Schwabe, P; Séré, A; Strub, PY;

Publicação
IACR Trans. Cryptogr. Hardw. Embed. Syst.

Abstract
In this paper we present the first formally verified implementations of Kyber and, to the best of our knowledge, the first such implementations of any post-quantum cryptosystem. We give a (readable) formal specification of Kyber in the EasyCrypt proof assistant, which is syntactically very close to the pseudocode description of the scheme as given in the most recent version of the NIST submission. We present high-assurance open-source implementations of Kyber written in the Jasmin language, along with machine-checked proofs that they are functionally correct with respect to the EasyCrypt specification. We describe a number of improvements to the EasyCrypt and Jasmin frameworks that were needed for this implementation and verification effort, and we present detailed benchmarks of our implementations, showing that our code achieves performance close to existing hand-optimized implementations in C and assembly.

2023

Formally verifying Kyber Part I: Implementation Correctness

Autores
Almeida, JB; Barbosa, M; Barthe, G; Grégoire, B; Laporte, V; Léchenet, JC; Oliveira, T; Pacheco, H; Quaresma, M; Schwabe, P; Séré, A; Strub, PY;

Publicação
IACR Cryptol. ePrint Arch.

Abstract

2023

Leakage-Free Probabilistic Jasmin Programs

Autores
Almeida, JB; Firsov, D; Oliveira, T; Unruh, D;

Publicação
IACR Cryptol. ePrint Arch.

Abstract

2022

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

Autores
Almeida, JCB; Barbosa, M; Barthe, G; Pacheco, H; Pereira, V; Portela, B;

Publicação
JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING

Abstract
Secure multiparty computation (SMC) allows for complex computations over encrypted data. Privacy concerns for cloud applications makes this a highly desired technology and recent performance improvements show that it is practical. To make SMC accessible to non-experts and empower its use in varied applications, many domain-specific compilers are being proposed.We review the role of these compilers and provide a formal treatment of the core steps that they perform to bridge the abstraction gap between high-level ideal specifications and efficient SMC protocols. Our abstract framework bridges this secure compilation problem across two dimensions: 1) language-based source- to target-level semantic and efficiency gaps, and 2) cryptographic ideal- to real-world security gaps. We link the former to the setting of certified compilation, paving the way to leverage long-run efforts such as CompCert in future SMC compilers. Security is framed in the standard cryptographic sense. Our results are supported by a machine-checked formalisation carried out in EasyCrypt.

Teses
supervisionadas

2023

Extending Conflict Free Replicated Data Types Fault Models

Autor
Houssam Ahmad Yactine

Instituição
UM

2022

Icarus - A Cloud Security Perspective

Autor
João Aloísio Sousa Araújo

Instituição
UM

2022

Implementação e verificação de código criptográfico com segurança pós-quântica

Autor
Henrique José Carvalho Faria

Instituição
UM

2022

Implementação Certificada da Componente Criptográfica do Gestor de Passwords KeePass

Autor
Pedro Miguel Marques Freitas

Instituição
UM

2022

Rastreabilidade e compromissos de segurança em veículos modernos

Autor
Mariana Pereira Fernandes

Instituição
UM