Alessandro Bruni

Security Protocol Verification

Overview

Security protocols are the backbone of secure communication, but subtle design flaws can undermine their guarantees. My work applies formal methods — model checking, abstraction-based verification, and choreographic approaches — to prove that protocols meet their security goals.

Key Topics

Protocol analysis with AIF-ω. I co-developed AIF-ω, a tool for set-based abstraction of stateful security protocols with countable families of agents. AIF-ω has been applied to protocols in automotive (MaCAN) and IoT settings.

EDHOC verification. I have led multiple formal analyses of the EDHOC key establishment protocol for constrained IoT devices, using the Tamarin prover to verify authentication, secrecy, and forward secrecy properties.

Cryptographic choreographies. Recent work explores how choreographic descriptions of security protocols can be used to derive correct implementations, combining ideas from session types and protocol verification.

E-voting security. I have analysed e-voting protocols including Selene and Bingo Voting, verifying properties such as receipt-freeness, vote privacy, and accountability.

Selected Publications