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.
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.
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.
I love chess, here are some of my favourite chess compositions (the board is interactive):