Disputas: Anders Moen Hagalisletto

Prøveforelesning

Bedømmelseskomité

Professor Willem Paul de Roever, Department of Informatics, University of Kiel
Assosciate Professor Monica Nesi, Department of Informatics, University of L’Aquila
Researcher Martin Steffen, Department of Informatics, University of Oslo

Leder av disputas:  Morten Dæhlen

Veileder:  Olaf Owe, Herman Ruge Jervell, Peter Csaba Ölveczky

Sammendrag

This thesis investigates the practical application of formal methods, with focus on high level design languages. In computer science and software engineering, formal methods are considered to be mathematically-based techniques for the specification, development and verification of software and hardware systems. The use of formal methods for software and hardware design is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analyses can contribute to the reliability and robustness of a design. The thesis presents the underlying mathematical framework for a tool that can discover errors and severe flaws in security protocols and attacks on such protocols. The method and tool developed in the thesis have been used to detect severe errors in attacks that were considered to be correct until recently and also to find many new real and potential attacks on a commercial protocol for secure mobile transactions. Since security protocols, like internet-bank or e-commerce protocols must be reliable, the tool has potential for being used in the software industry to support more trustworthy security applications.

Kontaktperson

For mer informasjon, kontakt Lena Korsnes.