Verification and validation of security protocol implementations

Abstract

Security protocols are important and widely used because they enable secure communication to take place over insecure networks. Over the years numerous formal methods have been developed to assist protocol designers by analysing models of these protocols to determine their security properties. Beyond the design stage however, developers rarely employ formal methods when implementing security protocols. This may result in implementation flaws often leading to security breaches. This dissertation contributes to the study of security protocol analysis by advancing the emerging field of implementation analysis. Two tools are presented which together translate between Java and the LySa process calculus. Elyjah translates Java implementations into formal models in LySa. In contrast, Hajyle generates Java implementations from LySa models. These tools and the accompanying LySa verification tool perform rapid static analysis and have been integrated into the Eclipse Development Environment. The speed of the static analysis allows these tools to be used at compile-time without disrupting a developer’s workflow. This allows us to position this work in the domain of practical software tools supporting working developers. As many of these developers may be unfamiliar with modelling security protocols a suite of tools for the LySa process calculus is also provided. These tools are designed to make LySa models easier to understand and manipulate. Additional tools are provided for performance modelling of security protocols. These allow both the designer and the implementor to predict and analyse the overall time taken for a protocol run to complete. Elyjah was among the very first tools to provide a method of translating between implementation and formal model, and the first to use either Java for the implementation language or LySa for the modelling language. To the best of our knowledge, the combination of Elyjah and Hajyle represents the first and so far only system which provides translation from both code to model and back again.