Elsa López Pérez

Work

Selected Projects

Time-Series ML · Personal Research

Python pandas FastAPI HRV · Sleep

Physiological Cycle Phase & Ovulation Prediction from Wearable Data

An end-to-end personal research project: built a privacy-preserving platform to collect longitudinal wearable data (heart-rate variability, resting HR, sleep architecture, stress, training load) from multiple participants, and a multi-class time-series pipeline to model physiological cycle phases — and detect ovulation — from continuous biosignals.

Built and deployed a participant data-collection system (FastAPI web app + packaged cross-platform desktop app) that gathers wearable data without ever storing user credentials, scaling the study beyond a single subject
Rolling-window feature engineering — lag features, past-only rolling means, and day-to-day deltas — capturing temporal patterns across HRV, sleep stages, and training load
Statistically validated that the follicular - luteal transition (ovulation) is detectable from resting HR and HRV (cycle-aligned analysis, paired tests, large effect sizes)

Cryptography · IoT Protocol

Rust no_std IETF LAKE

EDHOC-PSK — lakers crate

Core contributor to lakers, the reference Rust implementation of the EDHOC lightweight authenticated key exchange protocol (RFC 9528). I designed and implemented the Pre-Shared Key (PSK) authentication extension, working directly with IETF LAKE Working Group engineers to ensure interoperability across implementations and production readiness for constrained IoT hardware.

PSK extension enables EDHOC on devices with no PKI infrastructure, reducing handshake overhead
Supports both software backends (RustCrypto) and hardware-accelerated backends (STM32 PKA, Nordic CC310) through a unified abstraction layer
no_std, zero heap allocations — runs on ARM Cortex-M with kilobytes of RAM
C and Python bindings shipped alongside the core library

Formal Verification · Security Proofs

Tamarin ProVerif SAPIC+ Python

Formal Security Analysis of EDHOC-PSK

Symbolic security proofs for the EDHOC-PSK protocol extension, modelling authentication, secrecy, anonymity, and unlinkability under advanced adversary models, including post-quantum Save-Now-Decrypt-Later (SNDL) attackers. Published at ACM ASIACCS 2026.

Protocol models written in SAPIC+, automatically compiled to both Tamarin and ProVerif for cross-tool verification
Identified concrete authentication and identity-protection weaknesses under SNDL adversaries, fed back into the IETF standardization process
Dockerised automation scripts enable one-command reproduction of all proof results
Extended to 5G network attachment scenarios and remote attestation variants (separate repos)

Embedded Systems · Hardware Cryptography

Rust STM32 nRF54 ARM Cortex-M

embedded-cal — Formally Verified Cryptographic Provider

Co-designed with Cryspen a reusable Rust cryptographic abstraction layer that gives uniform access to hardware-accelerated and formally verified software primitives across ARM Cortex-M platforms. Received the Best Paper Award at SPT-IoT 2026.

Unified HAL over STM32 PKA, AES-256, SHA-256 (STM32WBA55) and Nordic CryptoCell/CC310 (nRF54) — no code changes needed to switch targets
Benchmarked execution time, flash usage, and power consumption: hardware acceleration delivers significant speedups over software-only implementations at the same security level
Memory safety and secret-independence guarantees preserved end-to-end, verified against the formally verified HACL* cryptographic library
Bare-metal STM32 driver experiments publicly available in the companion repository

Reinforcement Learning · Robotics

Python ROS Gazebo PPO

Multi-Robot Navigation with RVO-Shaped RL (Nokia Bell Labs)

At Nokia Bell Labs I integrated and re-trained a PPO-based multi-agent navigation policy within a full ROS robotics stack, then led the simulation-to-real transfer analysis to close the gap between Gazebo high-fidelity simulation and physical robot deployment.

Re-trained the policy with a Reciprocal Velocity Obstacle (RVO) shaped reward to improve collision avoidance in dense multi-robot scenarios
Diagnosed and resolved sim-to-real failures caused by sensing noise and actuation delay — improved navigation success rate to 98% in randomised high-fidelity scenarios
Designed multi-stage curriculum training pipeline (4 robots → 10 robots → 20 robots) to progressively increase task difficulty
Validated policy generalisation across circle and random initialisation scenarios with up to 20 simultaneous agents

Deep Learning · Computer Vision

PyTorch scikit-learn OpenCV

Semi-Supervised Deep Learning for Pharmaceutical Imaging (IBISC)

Built a semi-supervised classification pipeline for automated quality control of microscopic flow imaging (MFI) particle images in a pharmaceutical manufacturing context, addressing a dataset of over 190,000 images with significant class imbalance and label noise.

Convolutional Variational Autoencoder (VAE) trained to learn compact latent representations combining texture, shape, and geometric features
Semi-supervised approach leverages the large unlabelled pool — critical when expert annotation is expensive in regulated pharmaceutical environments
Improved binary classification accuracy from 70% to 86% after systematic class-imbalance correction and mislabelling audit
Evaluated with confusion matrices, PCA, t-SNE, and reconstruction loss to understand failure modes and latent space structure

High-Performance Computing · Parallel Algorithms

C MPI OpenMP Python

Parallel Dijkstra for HPC Clusters

Parallel implementations of Dijkstra's shortest-path algorithm for high-performance computing environments, comparing serial, OpenMP (shared-memory) and MPI (distributed-memory) strategies on randomly generated graphs and benchmarking their scaling on a computing cluster.

Three implementations — serial, OpenMP, and MPI — sharing a common graph-generation and benchmarking pipeline
Python tooling to generate random graphs and visualise results, with shell scripts for cluster job submission via qsub
Evaluated parallel speedup and scaling behaviour across varying graph sizes and core counts on an MPICH cluster

Data Mining · Recommendation Systems

Python Jupyter Query Mining

Query Recommendation & Importance Mining

A data mining project in two parts: a query recommendation system that suggests relevant queries to users, and a method to quantify the importance of a query to a given user — applied to a real-estate (house) search dataset.

Built a query recommendation engine from user–query interaction data
Designed a scoring method to estimate how important a query is to each user
Modular notebooks with reusable auxiliary and database-handling functions over JSON-backed data

Machine Learning · Statistical Theory

Python Gaussian Processes PAC-Bayes

Supervised Learning based on Gaussian Processes

Bachelor's thesis exploring the theoretical foundations of Gaussian process regression, its connection to kernel-based methods, and statistical regularization. Grounded theoretical results in experiments on real-world data.

Studied PAC-Bayesian performance guarantees for supervised learning, connecting theory to practice
Analysed the equivalence between Gaussian process regression and kernel ridge regression
Applied GP regression to a 7-DOF anthropomorphic robotic arm: mapping a 21-dimensional input space to the corresponding 7 torque outputs
Validated theoretical results through experiments on real-world datasets

Career

Experience & Education

Inria · Sorbonne Nov 2023 – Dec 2026
Paris, France

Inria – Sorbonne Université

PhD Researcher — Secure IoT Protocols

Designed, implemented, and formally verified the EDHOC-PSK authentication protocol for constrained IoT devices using SAPIC+
Identified authentication and identity-protection weaknesses under advanced adversary models including post-quantum attackers
Benchmarked performance and memory footprint on ARM Cortex-M platforms
Contributed protocol specifications directly to the IETF LAKE standardization process

Nokia Bell Labs Mar – Aug 2023
Paris, France

Nokia Bell Labs

Research Intern — Reinforcement Learning & Multi-Robot Systems

Integrated and re-trained a PPO-based multi-agent navigation policy within a ROS robotics stack
Led simulation-to-real transfer analysis, resolving deployment failures from sensing noise and actuation delays
Improved navigation success rate to 98% in randomised high-fidelity simulation

IBISC · Paris-Saclay May – Aug 2022
Évry, France

IBISC – Université Paris-Saclay

ML Intern — AI for Pharmaceutical Imaging

Built a semi-supervised deep learning pipeline for automated classification of 190k+ MFI particle images
Improved binary classification accuracy from 70% to 86% by addressing class imbalance and dataset mislabelling

Education 2016 – 2026

Academic Background

PhD · Master · Double Bachelor

PhD in Secure Protocols — Sorbonne Université & Inria (2023–2026)
EIT Digital Master in Data Science & AI — Université Paris-Saclay & Università di Trento (2021–2023)
Double Bachelor, Mathematics & Physics — Univ. of Valladolid & Univ. of Dundee, Erasmus (2016–2021)

Selected Projects

Physiological Cycle Phase & Ovulation Prediction from Wearable Data

EDHOC-PSK — lakers crate

Formal Security Analysis of EDHOC-PSK

embedded-cal — Formally Verified Cryptographic Provider

Multi-Robot Navigation with RVO-Shaped RL (Nokia Bell Labs)

Semi-Supervised Deep Learning for Pharmaceutical Imaging (IBISC)

Parallel Dijkstra for HPC Clusters

Query Recommendation & Importance Mining

Supervised Learning based on Gaussian Processes

Experience & Education

Inria – Sorbonne Université

Nokia Bell Labs

IBISC – Université Paris-Saclay

Academic Background

Selected Publications

embedded-cal: A Formally Verified Cryptographic Provider for Embedded Platforms 🏆 Best Paper

Formal Verification of EDHOC-PSK: A Symbolic Approach

Pre-Shared Key Authentication With EDHOC: The Security–Performance Tradeoff

EDHOC Authenticated with Pre-Shared Keys (PSK)

EDHOC is a New Security Handshake Standard

Skills

Languages

ML & Data Science

Formal Methods

Embedded & Hardware

Robotics

Standardization

Languages spoken

Beyond the terminal