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
Download foto HD

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
  • Cluster

    Informática
  • Cargo

    Investigador Coordenador
  • Desde

    01 novembro 2011
008
Publicações

2021

Secure Conflict-free Replicated Data Types

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

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

Abstract

2020

Decentralized Privacy-Preserving Proximity Tracing

Autores
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;

Publicação
CoRR

Abstract

2020

Universally Composable Relaxed Password Authenticated Key Exchange

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

Publicação
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

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

Publicação
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

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

Publicação
Progress in Cryptology - INDOCRYPT 2020 - 21st International Conference on Cryptology in India, Bangalore, India, December 13-16, 2020, Proceedings

Abstract

Teses
supervisionadas

2020

Trade-offs between privacy and efficiency on databases

Autor
Rogério António da Costa Pontes

Instituição
UP-FCUP

2020

Integrated Verification of Cryptographic Security Proofs and Implementations

Autor
Vítor Manuel Parreira Pereira

Instituição
UP-FEUP

2020

High-speed and High-assurance Cryptographic Software

Autor
Tiago Filipe Azevedo Oliveira

Instituição
UP-FCUP

2020

Interoperabilidade FIDO

Autor
Mateus de Campos

Instituição
UP-FCUP

2019

Trade-offs between privacy and efficiency on databases

Autor
Rogério António da Costa Pontes

Instituição
UP-FCUP