Cookies Policy
We use cookies to improve our site and your experience. By continuing to browse our site you accept our cookie policy. Find out More
Close
  • Menu
About

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

    Centre Coordinator
  • Since

    01st November 2011
005
Publications

2018

Indifferentiable Authenticated Encryption

Authors
Barbosa, M; Farshim, P;

Publication
Advances in Cryptology - CRYPTO 2018 - 38th Annual International Cryptology Conference, Santa Barbara, CA, USA, August 19-23, 2018, Proceedings, Part I

Abstract
We study Authenticated Encryption with Associated Data (AEAD) from the viewpoint of composition in arbitrary (single-stage) environments. We use the indifferentiability framework to formalize the intuition that a “good” AEAD scheme should have random ciphertexts subject to decryptability. Within this framework, we can then apply the indifferentiability composition theorem to show that such schemes offer extra safeguards wherever the relevant security properties are not known, or cannot be predicted in advance, as in general-purpose crypto libraries and standards. We show, on the negative side, that generic composition (in many of its configurations) and well-known classical and recent schemes fail to achieve indifferentiability. On the positive side, we give a provably indifferentiable Feistel-based construction, which reduces the round complexity from at least 6, needed for blockciphers, to only 3 for encryption. This result is not too far off the theoretical optimum as we give a lower bound that rules out the indifferentiability of any construction with less than 2 rounds. © International Association for Cryptologic Research 2018.

2018

Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks

Authors
Almeida, JB; Barbosa, M; Barthe, G; Pacheco, H; Pereira, V; Portela, B;

Publication
Proceedings - IEEE Computer Security Foundations Symposium

Abstract
We give a language-based security treatment of domain-specific languages and compilers for secure multi-party computation, a cryptographic paradigm that enables collaborative computation over encrypted data. Computations are specified in a core imperative language, as if they were intended to be executed by a trusted-third party, and formally verified against an information-flow policy modelling (an upper bound to) their leakage. This allows non-experts to assess the impact of performance-driven authorized disclosure of intermediate values. Specifications are then compiled to multi-party protocols. We formalize protocol security using (distributed) probabilistic information-flow and prove security-preserving compilation: Protocols only leak what is allowed by the source policy. The proof exploits a natural but previously missing correspondence between simulation-based cryptographic proofs and (composable) probabilistic non-interference. Finally, we extend our framework to justify leakage cancelling, a domain-specific optimization that allows to first write an efficient specification that fails to meet the allowed leakage upper-bound, and then apply a probabilistic pre-processing that brings leakage to the acceptable range. © 2018 IEEE.

2017

Jasmin: High-Assurance and High-Speed Cryptography

Authors
Almeida, JB; Barbosa, M; Barthe, G; Blot, A; Grégoire, B; Laporte, V; Oliveira, T; Pacheco, H; Schmidt, B; Strub, PY;

Publication
Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, Dallas, TX, USA, October 30 - November 03, 2017

Abstract

2017

A Fast and Verified Software Stack for Secure Function Evaluation

Authors
Almeida, JB; Barbosa, M; Barthe, G; Dupressoir, F; Gregoire, B; Laporte, V; Pereira, V;

Publication
Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, Dallas, TX, USA, October 30 - November 03, 2017

Abstract

2017

Performance trade-offs on a secure multi-party relational database

Authors
Pontes, R; Pinto, M; Barbosa, M; Vilaça, R; Matos, M; Oliveira, R;

Publication
Proceedings of the Symposium on Applied Computing, SAC 2017, Marrakech, Morocco, April 3-7, 2017

Abstract

Supervised
thesis

2017

High-speed and High-assurance Cryptographic Software

Author
Tiago Filipe Azevedo Oliveira

Institution
UP-FCUP

2017

Integrated verification of cryptographic security proofs and implementations

Author
Vitor Manuel Parreira Pereira

Institution
UP-FCUP

2017

Electronic Voting over the Internet - A real-world solution

Author
Michael Lothar Mendes Seufert

Institution
UP-FCUP

2016

Secure multi party computation trade-offs in distritubed databases

Author
Rogério António da Costa Pontes

Institution
UP-FCUP

2016

High-speed and high-assurance cryptographic software

Author
Tiago filipe Azevedo Oliveira

Institution
UP-FCUP