1 Department of Informatics and Mathematical Modeling, Technical University of Denmark2 Language-Based Technology, Department of Informatics and Mathematical Modeling, Technical University of Denmark3 Department of Applied Mathematics and Computer Science, Technical University of Denmark
It has for a long time been a challenge to built secure networking systems. One way to counter this problem is to provide developers of software applications for networking systems with easy-to-use tools that can check security properties before the applications ever reach the marked. These tools will both help raise the general level of awareness of the problems and prevent the most basic flaws from occurring. This thesis contributes to the development of such tools. Networking systems typically try to attain secure communication by applying standard cryptographic techniques. In this thesis such networking systems are modelled in the process calculus LySa. On top of this programming language based formalism an analysis is developed, which relies on techniques from data and control ow analysis. These are techniques that can be fully automated, which make them an ideal basis for tools targeted at non-experts users. The feasibility of the techiques is illustrated by a proof-of-concept implementation of a control ow analysis developed for LySa. From a techincal point of view, this implementation also interesting because it encodes in nite sets of algebraic terms, which denote encryption, as a nite number of tree grammar rules. The security of any software application relies crucially on the scenario in which the application is deployed. In contrast to many related analysis approaches, this thesis provides an explict mechanism for specifying deployment scenarios. Even though these scenarios may be arbitrarily large the analysis techniques can be extended to cope with such scenarios. The analysis techniques are furthermore capable of tackling security issues that arise because of attacks from arbitrary attackers: the analysis can deal with con dentiality and authentication properties, parallel session attacks, and attacks launched by insiders. Finally, the perspectives for the application of the analysis techniques are discussed, thereby, coming a small step closer to providing developers with easy- to-use tools for validating the security of networking applications.