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
Sobre

Sobre

Sou Professor Auxiliar no Departamento de Ciência de Computadores da Faculdade de Ciências da Universidade do Porto (DCC-FCUP) e investigador do HASLab/INESC TEC. Os meus interesses de investigação centram-se na Criptografia e Segurança da Informação e na sua intersecção com a Verificação de Programas.

Sou Doutorado em Electrical and Electronic Engineering pela Newcastle University, e licenciado em Engenharia Electrotécnica e de Computadores pela FEUP. Fui investigador visitante na University of Bristol, IT Porto e na École Normale Supérieure.

Trabalho no desenvolvimento de software criptográfico confiável há 10 anos, com o objectivo de estabelecer uma ligação entre a segurança teórica e a segurança de aplicações reais. Interesso-me particularmente pela segurança demonstrável e a sua ligação à verificação formal de provas de segurança e de implementações de software criptográfico.

Para informação sobre a minha investigação, projectos e publicações, por favor consultar a minha página no HASLab.

Para informação sobre as minhas actividades de ensino, por favor consultar a minha página institucional na FCUP.

Tópicos
de interesse
Detalhes

Detalhes

  • Nome

    Manuel Barbosa
  • Desde

    01 novembro 2011
007
Publicações

2024

Bare PAKE: Universally Composable Key Exchange from Just Passwords

Autores
Barbosa, M; Gellert, K; Hesse, J; Jarecki, S;

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

Abstract
In the past three decades, an impressive body of knowledge has been built around secure and private password authentication. In particular, secure password-authenticated key exchange (PAKE) protocols require only minimal overhead over a classical Diffie-Hellman key exchange. PAKEs are also known to fulfill strong composable security guarantees that capture many password-specific concerns such as password correlations or password mistyping, to name only a few. However, to enjoy both round-optimality and strong security, applications of PAKE protocols must provide unique session and participant identifiers. If such identifiers are not readily available, they must be agreed upon at the cost of additional communication flows, a fact which has been met with incomprehension among practitioners, and which hindered the adoption of provably secure password authentication in practice. In this work, we resolve this issue by proposing a new paradigm for truly password-only yet securely composable PAKE, called bare PAKE. We formally prove that two prominent PAKE protocols, namely CPace and EKE, can be cast as bare PAKEs and hence do not require pre-agreement of anything else than a password. Our bare PAKE modeling further allows to investigate a novel reusability property of PAKEs, i.e., whether n(2) pairwise keys can be exchanged from only n messages, just as the Diffie-Hellman non-interactive key exchange can do in a public-key setting. As a side contribution, this add-on property of bare PAKEs leads us to observe that some previous PAKE constructions relied on unnecessarily strong, reusable building blocks. By showing that non-reusable tools suffice for standard PAKE, we open a new path towards round-optimal post-quantum secure password-authenticated key exchange.

2024

C'est très CHIC: A compact password-authenticated key exchange from lattice-based KEM

Autores
Arriaga, A; Barbosa, M; Jarecki, S; Skrobot, M;

Publicação
IACR Cryptol. ePrint Arch.

Abstract
Driven by the NIST’s post-quantum standardization efforts and the selection of Kyber as a lattice-based Key-Encapsulation Mechanism (KEM), several Password Authenticated Key Exchange (PAKE) protocols have been recently proposed that leverage a KEM to create an efficient, easy-to-implement and secure PAKE. In two recent works, Beguinet et al. (ACNS 2023) and Pan and Zeng (ASIACRYPT 2023) proposed generic compilers that transform KEM into PAKE, relying on an Ideal Cipher (IC) defined over a group. However, although IC on a group is often used in cryptographic protocols, special care must be taken to instantiate such objects in practice, especially when a low-entropy key is used. To address this concern, Dos Santos et al. (EUROCRYPT 2023) proposed a relaxation of the IC model under the Universal Composability (UC) framework called Half-Ideal Cipher (HIC). They demonstrate how to construct a UC-secure PAKE protocol, EKE-KEM, from a KEM and a modified 2-round Feistel construction called m2F. Remarkably, the m2F sidesteps the use of an IC over a group, and instead employs an IC defined over a fixed-length bitstring domain, which is easier to instantiate. In this paper, we introduce a novel PAKE protocol called CHIC that improves the communication and computation efficiency of EKE-KEM, by avoiding the HIC abstraction. Instead, we split the KEM public key in two parts and use the m2F directly, without further randomization. We provide a detailed proof of the security of CHIC and establish precise security requirements for the underlying KEM, including one-wayness and anonymity of ciphertexts, and uniformity of public keys. Our findings extend to general KEM-based EKE-style protocols and show that a passively secure KEM is not sufficient. In this respect, our results align with those of Pan and Zeng (ASIACRYPT 2023), but contradict the analyses of KEM-to-PAKE compilers by Beguinet et al. (ACNS 2023) and Dos Santos et al. (EUROCRYPT 2023). Finally, we provide an implementation of CHIC, highlighting its minimal overhead compared to the underlying KEM – Kyber. An interesting aspect of the implementation is that we reuse the rejection sampling procedure in Kyber reference code to address the challenge of hashing onto the public key space. As of now, to the best of our knowledge, CHIC stands as the most efficient PAKE protocol from black-box KEM that offers rigorously proven UC security. © The Author(s), under exclusive license to Springer Nature Singapore Pte Ltd. 2025.

2024

X-Wing: The Hybrid KEM You've Been Looking For

Autores
Barbosa, M; Connolly, D; Duarte, JD; Kaiser, A; Schwabe, P; Varner, K; Westerbaan, B;

Publicação
IACR Cryptol. ePrint Arch.

Abstract

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.

2024

A Tight Security Proof for $\mathrm{SPHINCS^{+}}$, Formally Verified

Autores
Barbosa, M; Dupressoir, F; Hülsing, A; Meijers, M; Strub, PY;

Publicação
IACR Cryptol. ePrint Arch.

Abstract