Automated Analysis of Security in Networking Systems

Publication: ResearchPh.D. thesis – Annual report year: 2004

Standard

Automated Analysis of Security in Networking Systems. / Buchholtz, Mikael; Nielson, Hanne Riis (Supervisor); Nielson, Flemming (Supervisor).

2004. (IMM-PHD-2004-141).

Publication: ResearchPh.D. thesis – Annual report year: 2004

Harvard

APA

CBE

MLA

Vancouver

Author

Buchholtz, Mikael; Nielson, Hanne Riis (Supervisor); Nielson, Flemming (Supervisor) / Automated Analysis of Security in Networking Systems.

2004. (IMM-PHD-2004-141).

Publication: ResearchPh.D. thesis – Annual report year: 2004

Bibtex

@phdthesis{79e45943af32454894a7b3e5307a3054,
title = "Automated Analysis of Security in Networking Systems",
author = "Mikael Buchholtz and Nielson, {Hanne Riis} and Flemming Nielson",
year = "2004",
series = "IMM-PHD-2004-141",

}

RIS

TY - BOOK

T1 - Automated Analysis of Security in Networking Systems

A1 - Buchholtz,Mikael

AU - Buchholtz,Mikael

A2 - Nielson,Hanne Riis

A2 - Nielson,Flemming

ED - Nielson,Hanne Riis

ED - Nielson,Flemming

PY - 2004

Y1 - 2004

N2 - 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.

AB - 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.

UR - http://www.imm.dtu.dk/pubdb/p.php?3419

BT - Automated Analysis of Security in Networking Systems

T3 - IMM-PHD-2004-141

T3 - en_GB

ER -