Public defence in Computer Science, M.Sc. (Tech) Aleksi Peltonen

Title of the thesis: Formal Verification and Standardization of Security Protocols 

Doctoral student: Aleksi Peltonen
Opponent: Prof. Kristian Gjøsteen, Norwegian University of Science and Technology (NTNU), Norway
Custos: Prof. Tuomas Aura, Aalto University School of Science, Department of Computer Science

Thesis available for public display 10 days prior to the defence at: https://aaltodoc.aalto.fi/doc_public/eonly/riiputus/

Verifiable Security of Cryptographic Protocols

Secure communication over open networks is fundamental for many modern information systems. Previously centralized architectures are now often dependent on distributed computing and inter-system communication over the Internet. This decentralization of computational systems has increased the need for reliable, fast, and secure communication protocols. However, a core challenge in designing these protocols is ensuring their correctness and security before broad deployment. Standardized protocols, in particular, need to be thoroughly analyzed already in the design phase to avoid unnecessary revisions, which are often slow to deploy comprehensively. Formal verification methods can be used to support the development of cryptographic protocols by providing a way of analyzing the security of their design even before implementation. 

In this thesis, we contribute to the protocol standardization community by providing formal analyses of security protocols. The work covers both well-known, widely deployed protocols as well as ongoing drafts under standardization. In addition to analyzing protocol specifications for known vulnerabilities, we also strive to identify and unveil new weaknesses and attacks. The research goals of the work are twofold: (1) analyzing impactful security protocols to identify vulnerabilities and attack models, and (2) using the lessons learned from evaluating these protocols in the standardization process of a device bootstrapping protocol. The work can be seen as part of an initiative to provide formal proof of security for cryptographic protocols and as a demonstration of the usefulness of protocol verification in the standardization process.

Contact details:

Doctoral theses in the School of Science: https://aaltodoc.aalto.fi/handle/123456789/52