A Tool for the Formal Analysis of Symmetric Primitives
Name
Kristjan Krips
Abstract
The master thesis is about improving a tool that is used for analyzing the
security of symmetric primitives. This tool is named ProveIt and it can
help researchers to verify the correctness and security of protocols that use
symmetric primitives. Symmetric primitives are low-level symmetric-key al-
gorithms. When given such protocol, the probability of breaking its security
can be found by doing a finite number of reductions. However, it is not
convenient to do such proofs on paper and therefore a tool can assist the
researcher. ProveIt lets the user to choose which reductions to do on a given
protocol. After parsing a protocol into an abstract syntax tree, ProveIt lets
the user to transform the initial protocol one step at a time in order to find
the probability of a successful attack against it. After a finite number of
reductions the proof is complete and the probability of a successful attack is
found. However, currently ProveIt is able to do only a few reductions and
this limits the usability of the tool.
The goal of this thesis is to add new reductions to ProveIt so that it
would be possible to work with this tool using common techniques for proving
the security of symmetric primitives. In order to add reductions to ProveIt
it is necessary to analyze different symmetric primitives to find out which
reductions are required. In the thesis we describe the necessary subset of
transformations that are required for doing reduction based proofs. We show
where different transformations can be applied and define how they change
the security game. We prove for each transformation how they change the
security game. After giving a proof we can describe how we implemented
the transformations in ProveIt.
As a result of this thesis ProveIt will have the basic functionalities re-
quired for doing the security proofs of symmetric primitives. Besides that,
all the implemented reductions have been analyzed and their effect to the
security game has been proved.
Graduation Thesis language
English
Graduation Thesis type
Master - Computer Science
Supervisor(s)
Sven Laur
Defence year
2012