Beta 1


Title Verifying security protocols by combining static analysis and model checking
Author Teeselink, Egbert
Supervisor Nielson, Hanne Riis (Language-Based Technology, Department of Informatics and Mathematical Modeling, Technical University of Denmark, DTU, DK-2800 Kgs. Lyngby, Denmark)
Nielson, Flemming (Language-Based Technology, Department of Informatics and Mathematical Modeling, Technical University of Denmark, DTU, DK-2800 Kgs. Lyngby, Denmark)
Institution Technical University of Denmark, DTU, DK-2800 Kgs. Lyngby, Denmark
Thesis level Master's thesis
Year 2008
Abstract In systems that require secure communication between agents, the protocols that are designed to make this as secure as required, often prove to be the weakest link in ensuring security. As a result, a lot of research has recently been done on methods to automatically verify certain properties about these protocols, so that we may find and correct flaws before a protocol is put to use. LySa is a process calculus which has been specifically designed to specify the behaviour of security protocols. In contrast to many more common methods of specifying these protocols, LySa forces the author to be explicit about all details of the behaviour. The LySa Tool is a program that reads a protocol specified in the LySa calculus and uses static analysis techniques to verify certain properties. Because the LySa Tool over-approximates the behaviour of the protocol in its analysis, no absolute certainty is provided if the tool reports a flaw. Additionally, the tool’s output is often not enough to reconstruct an attack or to fix the flaw. By means of model checking, a common technology for verifying communicating systems, we hope to address these limitations. Using a toolset such as mCRL2, we gain absolute certainty about the behaviour of a protocol in a finite scenario and we can automatically construct an instance of an attack if a flaw is found. We conclude that model checking using mCRL2 and LySa’s static analysis can be combined into a strong and efficient means of verifying security protocols, and we describe how this can be done.
Series IMM-M.Sc.-2008-86
Fulltext
Original PDF ep08_86.pdf (1.77 MB)
Admin Creation date: 2009-01-13    Update date: 2009-01-13    Source: dtu    ID: 233920    Original MXD