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


Vitor is a PhD student under the MAP-i doctoral programme, developing his research at the Cryptography team of HASLab | INESC TEC.

He graduated in Computer Science at University of Beira Interior in 2013, where he started his contact with Cryptography, mainly in the field of Homomorphic Encryption.

In 2015, he completed his Master degree at University of Minho in Computer Science, where he specialised himself in Formal Methods in Software Engineering and in Cryptography. During the lecture year, he developed two cohesive projects: one in cooperation with Galois, where he explored post-quantum cryptographic algorithms in Cryptol, and one where he used a verification tool specific to the domain of Cryptography (EasyCrypt) to prove properties over probabilistic programs. 

His master thesis - "A deductive verification tool for cryptographic software" - focused on the construction of a deductive verification tool for the CAO language using the EasyCrypt toolset as a backend for the tool.

His research interests are focused in Cryptography and on how to apply Formal Methods in the verification of cryptographic primitives. In particular, he is interested in the verifiable security and in the provable security topics.



  • Name

    Vítor Parreira Pereira
  • Cluster

    Computer Science
  • Role

    External Research Collaborator
  • Since

    01st January 2015


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

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

Proceedings - IEEE Computer Security Foundations Symposium

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.


A Fast and Verified Software Stack for Secure Function Evaluation

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

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