Cookies Policy
The website need some cookies and similar means to function. If you permit us, we will use those means to collect data on your visits for aggregated statistics to improve our service. Find out More
Accept Reject
  • Menu
Publications

Publications by Manuel Barbosa

2023

Mechanized Proofs of Adversarial Complexity and Application to Universal Composability

Authors
Barbosa, M; Barthe, G; Gregoire, B; Koutsos, A; Strub, PY;

Publication
ACM TRANSACTIONS ON PRIVACY AND SECURITY

Abstract
In this work, we enhance the EasyCrypt proof assistant to reason about the computational complexity of adversaries. The key technical tool is a Hoare logic for reasoning about computational complexity (execution time and oracle calls) of adversarial computations. Our Hoare logic is built on top of the module system used by EasyCrypt for modeling adversaries. We prove that our logic is sound w.r.t. the semantics of EasyCrypt programs-we also provide full semantics for the EasyCrypt module system, which was lacking previously. We showcase (for the first time in EasyCrypt and in other computer-aided cryptographic tools) how our approach can express precise relationships between the probability of adversarial success and their execution time. In particular, we can quantify existentially over adversaries in a complexity class and express general composition statements in simulation-based frameworks. Moreover, such statements can be composed to derive standard concrete security bounds for cryptographic constructions whose security is proved in a modular way. As a main benefit of our approach, we revisit security proofs of some well-known cryptographic constructions and present a new formalization of universal composability.

2023

Fixing and Mechanizing the Security Proof of Fiat-Shamir with Aborts and Dilithium

Authors
Barbosa, M; Barthe, G; Doczkal, C; Don, J; Fehr, S; Grégoire, B; Huang, YH; Hülsing, A; Lee, Y; Wu, XD;

Publication
ADVANCES IN CRYPTOLOGY - CRYPTO 2023, PT V

Abstract
We extend and consolidate the security justification for the Dilithium signature scheme. In particular, we identify a subtle but crucial gap that appears in several ROM and QROM security proofs for signature schemes that are based on the Fiat-Shamir with aborts paradigm, including Dilithium. The gap lies in the CMA-to-NMA reduction and was uncovered when trying to formalize a variant of the QROM security proof by Kiltz, Lyubashevsky, and Schaffner (Eurocrypt 2018). The gap was confirmed by the authors, and there seems to be no simple patch for it. We provide new, fixed proofs for the affected CMA-to-NMA reduction, both for the ROM and the QROM, and we perform a concrete security analysis for the case of Dilithium to show that the claimed security level is still valid after addressing the gap. Furthermore, we offer a fully mechanized ROM proof for the CMA-security of Dilithium in the EasyCrypt proof assistant. Our formalization includes several new tools and techniques of independent interest for future formal verification results.

2023

Rogue key and impersonation attacks on FIDO2: From theory to practice

Authors
Barbosa, M; Cirne, A; Esquível, L;

Publication
Proceedings of the 18th International Conference on Availability, Reliability and Security

Abstract

2024

Bare PAKE: Universally Composable Key Exchange from Just Passwords

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

Publication
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

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

Publication
IACR Cryptol. ePrint Arch.

Abstract

2024

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

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

Publication
IACR Cryptol. ePrint Arch.

Abstract

  • 19
  • 20