Analysis of Security Protocols by Annotations

The trend in Information Technology is that distributed systems and networks are becoming increasingly important, as most of the services and opportunities that characterise the modern society are based on these technologies. Communication among agents over networks has therefore acquired a great deal of research interest. In order to provide effective and reliable means of communication, more and more communication protocols are invented, and for most of them, security is a significant goal. It has long been a challenge to determine conclusively whether a given protocol is secure or not. The development of formal techniques, e.g. control flow analyses, that can check various security properties, is an important tool to meet this challenge. This dissertation contributes to the development of such techniques. In this dissertation, security protocols are modelled in the process calculus LYSA. A variety of interesting security properties that protocols are often expected to have are formalised: authentication, confidentiality, freshness, absence of simple and complex type flaws. Those security properties are explicitly specified as annotations embedded in the LYSA syntax. Finally, a number of automatic techniques for the analysis of system behaviour are developed. These techniques are specified as control flow analyses and are, therefore, guaranteed to terminate. The perspectives for the analysis techniques are discussed. Thus the dissertation marks a step forward both for scientists, who gain a general framework for the study of several interesting security properties, and developers, who get a collection of tools that can validate protocols with respect to various aspects of security.