Alessandro Bruni

Interests

Formal methods, logics, protocol verification and model checking.

Reverse bio

Starting February 2020, I am Associate Professor in Computer Security at the IT-University of Copenhagen. Previously, I worked as a Postdoc in Carsten Shürmann’s group at the IT-University of Copenhagen, working on the Meta-CLF project. I obtained my Ph.D. at the Technical University of Denmark, under supervision of Flemming Nielson and Hanne Riis Nielson, working on formal methods, security protocol verification and model checking, and before that I did my B.Sc. and M.Sc. at the University of Padova, Italy, graduating under supervision of Paolo Baldan.

Upcoming events

Teaching

Tools

MathComp-Analysis is a formalization of mathematical analysis. I contribute a formalization of probability theory.

AIF-Omega is an abstraction based verification tool for security protocols where participants have state that is beyond a single session.

SetPi (Now being merged with AIF-Omega) is an extension of the Applied Pi-calculus with support for persistent state, expressible in terms of names that can grow and shrink over time.

CPNunf is an unfolder for contextual Petri nets, an extension of this formalism with semantics to support concurrent read access to shared resources

Publications

Conference papers

  1. Reynald Affeldt, Alessandro Bruni, Cyril Cohen, Pierre Roux, Takafumi Saikawa: Formalizing concentration inequalities in Rocq: infrastructure and automation. ITP 2025 (to appear)
  2. Jairo Miguel Marulanda-Giraldo, Ekaterina Komendantskaya, Alessandro Bruni, Reynald Affeldt, Matteo Capucci, Enrico Marchioni: Our Ongoing Work: Quantifiers for Differentiable Logics in Rocq SAIV 2025 (to appear)
  3. Reynald Affeldt, Alessandro Bruni, Ekaterina Komendantskaya, Natalia Slusarz, Kathrin Stark: Taming Differentiable Logics with Coq Formalisation. ITP 2024 arXiv PDF
  4. Reynald Affeldt, Clark W. Barrett, Alessandro Bruni, Ieva Daukantas, Harun Khan, Takafumi Saikawa, Carsten Schürmann: Robust Mean Estimation by All Means (Short Paper). ITP 2024 PDF
  5. Alessandro Bruni, Eike Ritter, Carsten Scürmann: Skolemization for Intuitionistic Linear Logic. IJCAR 2024 arXiv
  6. Karl Norrman, Vaishnavi Sundararajan, Alessandro Bruni: Extended Formal Analysis of the EDHOC Protocol in Tamarin. ICETE (Selected Papers) 2021 (published 2023)
  7. Alessandro Bruni, Marco Carbone, Rosario Giustolisi, Sebastian Moedersheim, Carsten Schürmann: Security Protocols as Choreographies. Protocols, Strands, and Logic - Essays Dedicated to Joshua Guttman on the Occasion of his 66.66th Birthday
  8. Ieva Daukantas, Alessandro Bruni, Carsten Schürmann: Trimming Data Sets: a Verified Algorithm for Robust Mean Estimation. PPDP 2021
  9. Karl Norrman, Vaishnavi Sundararajan, Alessandro Bruni: Formal Analysis of EDHOC Key Establishment for Constrained IoT Devices. SECRYPT 2021
  10. Rosario Giustolisi, Alessandro Bruni: Privacy-Preserving Dispute Resolution in the Improved Bingo Voting. E-VOTE-ID 2020
  11. Karl Norrman, Vaishnavi Sundararajan, Alessandro Bruni: Formal Analysis of EDHOC Key Establishment for Constrained IoT Devices. CoRR abs/2007.11427 (2020)
  12. Carsten Schürmann, Alessandro Bruni; Technical and Socio-Technical Attacks on the Danish Party Endorsement System. E-VOTE-ID 2019
  13. Theis Grønbech Petersen, Thorvald Sahl Jørgensen, Alessandro Bruni and Carsten Schürmann; “Formal Verification of Ephemeral Diffie-Hellman Over COSE (EDHOC)”. Security Standardisation Research, Third International Conference, 2018 [Preprint]
  14. Alessandro Bruni, Rosario Giustolisi, Carsten Schürmann; Automated Analysis of Accountability. 20th Information Security Conference (ISC), 2017 [Slides]
  15. Eva Drewsen, Alessandro Bruni, Carsten Schürmann; Towards a Mechanized Proof of Selene Receipt-Freeness and Vote-Privacy. Second International Joint Conference on Electronic Voting, 2017 [Slides]
  16. Peter Brottveit Bock, Alessandro Bruni, Agata Murawska and Carsten Schürmann: Representing Session Types. Dale Miller’s Festschrift, 2016
  17. Michael Denzel, Alessandro Bruni and Mark Ryan. Smart-Guard: Defending User Input from Malware. The 13th IEEE International Conference on Advanced and Trusted Computing, 2016
  18. Sebastian Mödersheim and Alessandro Bruni. AIF-ω: Set-Based Protocol Abstraction with Countable Families. Principles of Security and Trust, 2016 [Preprint]
  19. Alessandro Bruni, Sebastian Mödersheim, Flemming Nielson and Hanne Riis Nielson. Set-pi: Set Membership Pi-calculus. Computer Security Foundations, 2015 [Extended version with corrections]
  20. Alessandro Bruni, Michal Sojka, Flemming Nielson and Hanne Riis Nielson. Formal Security Analysis of the MaCAN Protocol. Integrated Formal Methods, 2014
  21. Vigo, Roberto, Alessandro Bruni, and Ender Yüksel. Security Games for Cyber-Physical Systems. Secure IT Systems. Springer Berlin Heidelberg, 2013. 17-32.
  22. Baldan, P., Bruni, A., Corradini, A., König, B., & Schwoon, S. On the computation of McMillan’s prefix for contextual nets and graph grammars. Graph Transformations, 2010. 91-106.

Journal papers

  1. Baldan, P., Bruni, A., Corradini, A., König, B., Rodríguez, C., & Schwoon, S. Efficient unfolding of contextual Petri nets. Theoretical Computer Science, 2012.

Posters and Workshop Papers

  1. Reynald Affeldt, Alessandro Bruni, Pierre Roux, Takafumi Saikawa: Yet another formal theory of probabilities in Coq. TYPES 2024 slides abstract
  2. Alessandro Bruni, Sebastian Mödersheim, Flemming Nielson, Hanne Riis Nielson. Verification of Stateful Protocols, Set-based Abstractions in the Applied π-Calculus. Secure IT Systems, 2014.
  3. Alessandro Bruni, Markulf Kohlweiss, Myrto Arapinis, Mark D. Ryan, Eike Ritter, Flemming Nielson, and Hanne Riis Nielson. “Proving Stateful Injective Agreement with Refinement Types”. Cryptoforma Workshop, 2015. [Paper]

Thesis

  1. Alessandro Bruni. Analysis of Security Protocols in Embedded Systems. PhD thesis, DTU, 2016. [Link]

Past events