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