Formal methods, logics, protocol verification and model checking.
Starting February 2017, I am Assistant 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.
- 24-27 Oct 2017: Paper accepted at E-Vote-ID 2017 Towards a Mechanized Proof of Selene Receipt-Freeness and Vote-Privacy, with Eva Drewsen and Carsten Schürmann
- 3 Sep 2017: First International Workshop on Trends in Mechanized Secruity Proofs
- 7-8 Aug 2017: EASSS Summer school Presenting the analysis of security protocols in AIF-omega, with case studies in automotive
- 30 May 2017: Oresund Security Day ‘17, Resolution in linear logic, joint work with Eike Ritter and Carsten Schürmann
- Security, ITU, Spring 2018
- Critical Systems Seminar and Project, ITU, Fall 2017
- Discrete Mathematics, ITU, Fall 2017
- Critical Systems Seminar, ITU, Fall 2016
- Ethical Hacking Club, ITU (Facebook group)
- Supervising Theses:
- Formal Analysis of BlockChain in EasyCrypt, Oscar Felipe Cerda Toro, 2018
- Verifying Selene in Tamarin, Eva Drewsen, 2017
- Voting Protocol in Ethereum, Adrian Brink, 2017
- Transparent authentication with wearable devices, Jacob Cholewa and Rasmus Wismann, 2017
- Hacking WinVote machines, Florin Vasile and Andreas Nielsen, 2016
AIF-Omega is an abstraction based verification tool for security protocols where participants have state that is beyond a single session.
SetPi 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
- Alessandro Bruni, Rosario Giustolisi, Carsten Schürmann; Automated Analysis of Accountability. 20th Information Security Conference (ISC), 2017 [Slides]
- 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]
- Peter Brottveit Bock, Alessandro Bruni, Agata Murawska and Carsten Schürmann: Representing Session Types. Dale Miller’s Festschrift, 2016
- 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
- Sebastian Mödersheim and Alessandro Bruni. AIF-ω: Set-Based Protocol Abstraction with Countable Families. Principles of Security and Trust, 2016 [Preprint]
- Alessandro Bruni, Sebastian Mödersheim, Flemming Nielson and Hanne Riis Nielson. Set-pi: Set Membership Pi-calculus. Computer Security Foundations, 2015 [Preprint]
- Alessandro Bruni, Michal Sojka, Flemming Nielson and Hanne Riis Nielson. Formal Security Analysis of the MaCAN Protocol. Integrated Formal Methods, 2014
- Vigo, Roberto, Alessandro Bruni, and Ender Yüksel. Security Games for Cyber-Physical Systems. Secure IT Systems. Springer Berlin Heidelberg, 2013. 17-32.
- 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.
- 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
- 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.
- 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]
- Alessandro Bruni. Analysis of Security Protocols in Embedded Systems. PhD thesis, DTU, 2016. [Link]
- 07 Sep. 2016: “Selene in Celf: Formalising Voting Protocols in Linear Logic”, Invited talk at the University of Luxembourg [Slides]
- 16 Sep. 2016: Presenting AIF-ω at Lamas Sing 2016, [Slides].
- 26 Apr. 2016: Giving a talk at MF#K, on F* and the verification of security protocols [Slides]
- Jan 2016: “AIF-ω: Set-Based Protocol Abstraction with Countable Families” accepted at POST-2016