Miguel Ambrona

I am a post-doctoral researcher in the area of Cryptography at NTT Secure Platform Laboratories (Tokyo), under the supervision of Masayuki Abe.

Before joining NTT, I was a PhD student in Software, Systems and Computing at the IMDEA Software Institute and Universidad Politécnica de Madrid, under the supervision of Gilles Barthe and Benedikt Schmidt. After that, and prior to joining NTT, I stayed at IMDEA as a post-doctoral researcher, supervised by Dario Fiore and Claudio Soriente.

Previously, I studied Mathematical Engineering at Universidad Complutense de Madrid.

Research Interests

  • Computer-aided cryptography
  • Functional Programming
  • Generic Group Model
  • Attribute-Based Encryption
  • Functional Encryption
  • Simulation-based security
  • Zero-Knowledge Proofs
  • Isogeny-based cryptography


NTT Laboratories
3-9-11 Midori-cho, Musashino-shi
Tokyo, 180-8585 (JAPAN)



PhD in Software, Systems and Computing

Universidad Politécnica de Madrid and IMDEA Software Institute
Sep 2014 - Oct 2018

MS in Mathematical Engineering

Universidad Complutense de Madrid

BS in Mathematical Engineering

Universidad Complutense de Madrid


NTT Secure Platform Laboratories (Tokyo)

Under the supervision of Masayuki Abe
May 2017 - Sep 2017

Fábrica Nacional de Moneda y Timbre - RCM (Madrid)

Under the supervision of Luis Borruel


PhD Thesis

“Automated Analysis of Cryptographic Constructions”

Universidad Politécnica de Madrid, October 2018

In this thesis we develop new techniques and tools to broaden the scope of computer-aided cryptography, with special emphasis on pairing-based cryptography. More concretely, our methods are oriented to automatically analyzing the security of signature-like primitives and attribute-based encryption in the generic group model, achieving stronger security requirements compared to previous work on automated analysis. We also study indifferentiability of symmetric-key constructions (such as Feistel Networks or the Even-Mansour cipher) and explore how to automatically synthetize indifferentiability attacks.

All our contributions share a common methodology: we leverage techniques from formal methods, expressing cryptographic constructions and security definitions in a symbolic language. We then provide computational soundness theorems for such symbolic models that guarantee that the conclusions derived symbolically can be lifted to the actual (non-symbolic) model.


Master's Thesis

“The Green Vehicle Routing Problem with Multiple Technologies and Partial Recharges”

Universidad Complutense de Madrid, July 2014

We formulate and study a variant of the well-known vehicle routing problem, one in which the fleet consists of electric vehicles with a limited range, so they need to recharge their batteries in refueling stations.

We develop two integer linear programming models for exact resolution of the problem. It is remarkable that, improving on previous works, our models do not duplicate the graph nodes corresponding to refueling stations, which significantly decreases the number of integer variables in the system. Consequently, our models can compute the exact solution of problems where previous methods fail. However, for larger problems, even our exact models fall short, because their exact resolution requires excessive computing time. Alternatively, we develop heuristic algorithms to find relatively good solutions, though possibly not optimal, within short running times. Furthermore, we adapt and implement three metaheuristic techniques (simulated annealing, tabu search and variable neighbourhood search) and applied them to several test cases.



Generic Group Analyzer Unbounded

I am one of the main developers of the Generic Group Analyzer Unbounded, a tool that automatically analyzes the security of cryptographic constructions in the generic group model.

Generic Group Model Symbolic Solver

I am one of the main developers of the Generic Group Model Symbolic Solver, an extension of the previous tool that captures polynomial divisions in the exponent.

Attribute-Based Encryption

I developed a proof of concept implementation of attribute-based encryption in the framework of predicate encodings and pair encodings.

Indifferentiability Analysis

I developed a tool to perform computer-asisted analysis of cryptographic primitives in the framework of indifferentiability. This tool corresponds to the implementation of the techniques developed in Chapter 6 of my PhD Thesis and it is still work in progress.



“Black-Box Language Extension of Non-Interactive Zero-Knowledge Arguments”

Masayuki Abe, Miguel Ambrona, Miyako Ohkubo. Preprint


“Lower Bounds on Structure-Preserving Signatures for Bilateral Messages”

Masayuki Abe, Miguel Ambrona, Miyako Ohkubo and Mehdi Tibouchi. SCN 2018


“Attribute-Based Encryption in the Generic Group Model: Automated Proofs and New Constructions”

Miguel Ambrona, Gilles Barthe, Romain Gay and Hoeteck Wee. ACM CCS 2017

“Generic Transformations of Predicate Encodings: Constructions and Applications”

Miguel Ambrona, Gilles Barthe, Benedikt Schmidt. Crypto 2017


“Automated Unbounded Analysis of Cryptographic Constructions in the Generic Group Model”

Miguel Ambrona, Gilles Barthe, Benedikt Schmidt. Eurocrypt 2016


“Secure color. Advanced color techniques for analysis and security”

Luis Borruel, Miguel Ambrona. Fábrica Nacional de Moneda y Timbre.


I love chess, here are some of my favourite chess compositions (the board is interactive):