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
About
Download Photo HD

About

I am a lecturer at the Department of Computer Science in the Faculty of Science of the University of Porto (DCC-FCUP) and a researcher at HASLab/INESC TEC. My research interests lie in Cryptography and Information Security and its intersection with Program Verification.

I hold a Ph.D. in Electrical and Electronic Engineering from the Newcastle University, an M.Sc. from the same University, and a degree in Electrical and Computer Engineering from the Faculty of Engineering of the University of Porto. In the past I have been a visiting researcher at the University of Bristol, IT Porto and École Normale Supérieure.

I have been working on the development of high-assurance cryptographic implementations for the last 10 years, aiming to bridge the gap between theoretical security and real-world security. I am particularly interested in provable security and its interplay with the formal verification of cryptographic proofs and cryptographic software implementations.

For information on my research, projects and publications, please see my page at HASLab.

For information on my teaching activities, please see my institutional page at FCUP.

Interest
Topics
Details

Details

  • Name

    Manuel Barbosa
  • Cluster

    Computer Science
  • Role

    Research Coordinator
  • Since

    01st November 2011
010
Publications

2021

Secure Conflict-free Replicated Data Types

Authors
Barbosa, M; Ferreira, B; Marques, JC; Portela, B; Preguiça, NM;

Publication
ICDCN '21: International Conference on Distributed Computing and Networking, Virtual Event, Nara, Japan, January 5-8, 2021.

Abstract

2020

Decentralized Privacy-Preserving Proximity Tracing

Authors
Troncoso, C; Payer, M; Hubaux, JP; Salathé, M; Larus, JR; Bugnion, E; Lueks, W; Stadler, T; Pyrgelis, A; Antonioli, D; Barman, L; Chatel, S; Paterson, KG; Capkun, S; Basin, DA; Beutel, J; Jackson, D; Roeschlin, M; Leu, P; Preneel, B; Smart, NP; Abidin, A; Gürses, SF; Veale, M; Cremers, C; Backes, M; Tippenhauer, NO; Binns, R; Cattuto, C; Barrat, A; Fiore, D; Barbosa, M; Oliveira, R; Pereira, J;

Publication
CoRR

Abstract

2020

Universally Composable Relaxed Password Authenticated Key Exchange

Authors
Abdalla, M; Barbosa, M; Bradley, T; Jarecki, S; Katz, J; Xu, JY;

Publication
Advances in Cryptology - CRYPTO 2020 - 40th Annual International Cryptology Conference, CRYPTO 2020, Santa Barbara, CA, USA, August 17-21, 2020, Proceedings, Part I

Abstract
Protocols for password authenticated key exchange (PAKE) allow two parties who share only a weak password to agree on a cryptographic key. We revisit the notion of PAKE in the universal composability (UC) framework, and propose a relaxation of the PAKE functionality of Canetti et al. that we call lazy-extraction PAKE (lePAKE). Our relaxation allows the ideal-world adversary to postpone its password guess until after a session is complete. We argue that this relaxed notion still provides meaningful security in the password-only setting. As our main result, we show that several PAKE protocols that were previously only proven secure with respect to a “game-based” definition of security can be shown to UC-realize the lePAKE functionality in the random-oracle model. These include SPEKE, SPAKE2, and TBPEKE, the most efficient PAKE schemes currently known. © International Association for Cryptologic Research 2020.

2020

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

Authors
Almeida, JB; Barbosa, M; Barthe, G; Gregoire, B; Koutsos, A; Laporte, V; Oliveira, T; Strub, PY;

Publication
2020 IEEE Symposium on Security and Privacy, SP 2020, San Francisco, CA, USA, May 18-21, 2020

Abstract
We develop a new approach for building cryptographic implementations. Our approach goes the last mile and delivers assembly code that is provably functionally correct, protected against side-channels, and as efficient as hand-written assembly. We illustrate our approach using ChaCha20-Poly1305, one of the two ciphersuites recommended in TLS 1.3, and deliver formally verified vectorized implementations which outperform the fastest non-verified code.We realize our approach by combining the Jasmin framework, which offers in a single language features of high-level and low-level programming, and the EasyCrypt proof assistant, which offers a versatile verification infrastructure that supports proofs of functional correctness and equivalence checking. Neither of these tools had been used for functional correctness before. Taken together, these infrastructures empower programmers to develop efficient and verified implementations by "game hopping", starting from reference implementations that are proved functionally correct against a specification, and gradually introducing program optimizations that are proved correct by equivalence checking.We also make several contributions of independent interest, including a new and extensible verified compiler for Jasmin, with a richer memory model and support for vectorized instructions, and a new embedding of Jasmin in EasyCrypt. © 2020 IEEE.

2020

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

Authors
Almeida, JB; Barbosa, M; Barthe, G; Laporte, V; Oliveira, T;

Publication
Progress in Cryptology - INDOCRYPT 2020 - 21st International Conference on Cryptology in India, Bangalore, India, December 13-16, 2020, Proceedings

Abstract

Supervised
thesis

2020

Trade-offs between privacy and efficiency on databases

Author
Rogério António da Costa Pontes

Institution
UP-FCUP

2020

Interoperabilidade FIDO

Author
Mateus de Campos

Institution
UP-FCUP

2020

Integrated Verification of Cryptographic Security Proofs and Implementations

Author
Vítor Manuel Parreira Pereira

Institution
UP-FEUP

2020

High-speed and High-assurance Cryptographic Software

Author
Tiago Filipe Azevedo Oliveira

Institution
UP-FCUP

2019

High-speed and High-assurance Cryptographic Software

Author
Tiago Filipe Azevedo Oliveira

Institution
UP-FCUP