Abstract:


A Formalization of an Operational Semantics 
of Security Protocols


Simon Meier



As a result of the last twenty years of research 
on the veri?cation of security protocols, there 
exists now a range of protocol models, security 
properties, logics and veri?cation tools. Finding 
attacks on a ?awed protocol can nowadays be done 
e?ciently using tools such as Scyther [12]. However, 
the highest level of the Common Criteria (ISO 15408) 
requires a formal veri?cation of protocol 
correctness. Doing this strictly formal is still 
not possible, because of the lack of strictly 
formal protocol models with an associated veri?cation 
technique.In this diploma thesis, we present a 
conservative embedding in Isabelle/HOL [20] of the 
protocol model given by the operational semantics 
of security protocols proposed in [11]. This 
formalization is an important milestone towards the 
strictly formal veri?cation of security protocols. 
Its bene?ts are twofold: First, it is an unambiguous 
description of a protocol model, which greatly 
facilitates communicating results. Second, it enables 
the development of a protocol veri?cation technique 
with machine checkable proofs. This technique may 
make logically sound use of specialized protocol 
logics as well as automation provided by tools like 
Scyther.