@MASTERSTHESIS\{IMM2004-03228, author = "N. H. Kaplan", title = "Analysis and reconstruction of attacks on authentication protocols", year = "2004", keywords = "Authentication Protocols, Security protocols, Static Analysis, Control flow analysis, Model Checking, LySa, samc", school = "Informatics and Mathematical Modelling, Technical University of Denmark, {DTU}", address = "Richard Petersens Plads, Building 321, {DK-}2800 Kgs. Lyngby", type = "", note = "Supervised by Professor Hanne Riis Nielson", url = "http://www2.compute.dtu.dk/pubdb/pubs/3228-full.html", abstract = "In this project I use and develop methods for analyzing and reconstructing attacks on authentication protocols. I will combine two approaches to analysis of authentication protocols: Static analysis and model checking. The static analysis gives an over-approximation of the breaches of a protocol. My task is to choose a potential breach of a certain protocol, and if possible reconstruct the trace of events leading to this breach using techniques from model checking. The model checking will be aided by additional results from the analysis. The result of my work is a tool which makes it possible to efficiently find and reconstruct a certain breach of a given authentication protocol. In Danish: I dette projekt bruger og udvikler jeg metoder til at analysere og rekonstruere angreb p{\aa} autentifikationsprotokoller. Jeg kombinerer to tilgange til analyse af autentifikationsprotokoller: Statisk analyse og model checking. Statisk analyse giver en overapproksimation til fejl i en protokol. Min opgave er at v{\ae}lge en potentiel fejl i en given protokol og hvis muligt rekonstruere den sekvens af kommunikation, der for{\aa}rsager denne fejl. Til denne rekonstruktion benyttes model checking teknikker. Resultatet af mit arbejde er et v{\ae}rkt{\o}j, der g{\o}r det muligt effektivt at finde og rekonstruere en fejl i en given autentifikationsprotokol." }