UT Institute of Computer Science Graduation Theses Registry

Name

Pille Pullonen

Abstract

The aim of this paper was to describe a cryptographic protocol analyser, specially its protocol representation, and implement a transformation to simplify protocol representation. The analyser was first described in the doctoral thesis of Ilja Tšahhirov and was afterwards implemented by Peeter Laud and Ilja Tšahhirov. The analyser is designed for static protocol analysis to check confidentiality and integrity of secret messages. All cryptographic primitives used in the protocols have to be strong in computational model in order for the analysis to be correct. Protocols are represented by dependency flow graphs that indicate possible data and control flows in protocol execution. Like any directed graphs, they may contain directed cycles that make understanding and drawing graphs more difficult. In general, all nodes in graph can be divided to two groups - strict and non-strict nodes. Strict nodes only compute their value if they have received all their inputs, on the other hand, non-strict nodes compute their value as soon as they have sufficient inputs to do so. All cycles in graph can be divided to groups depending on which non-strict nodes they contain and how many of them are present. The analyser already has transformations to cut cycles with none or just one non-strict nodes. This paper described a way based on depth-first search trees to find all cycles and transform them so that they contain only one non-strict node and can therefore be removed by cutting an edge in the cycle.

Graduation Thesis language

Estonian

Graduation Thesis type

Bachelor - Computer Science

Supervisor(s)

Peeter Laud

Defence year

2011