Title 
Static Analysis for Protocol Validation in Hierarchical Networks 
Author

Zhang, Ye (Computer Science and Engineering, Department of Informatics and Mathematical Modeling, Technical University of Denmark, DTU, DK2800 Kgs. Lyngby, Denmark)

Supervisor

Nielson, Hanne Riis (LanguageBased Technology, Department of Informatics and Mathematical Modeling, Technical University of Denmark, DTU, DK2800 Kgs. Lyngby, Denmark)

Institution 
Technical University of Denmark, DTU, DK2800 Kgs. Lyngby, Denmark 
Thesis level 
Master's thesis 
Year 
2005 
Abstract 
The ambient calculus presents a highlevel view of mobile computation and gives rise to a highlevel treatment of the related security issues. Ambients, which are named bounded places, allow us to model the concept of local networks in a natural way. The tree structure formed by ambients just captures the characteristic of our interested network, the hierarchical network.
In this M.Sc. thesis, we focus on validating cryptographic protocols working on hierarchical networks. We begin with extending Boxed Ambients with annotations which declare the authentication intentions of cryptographic protocols. We then develop a static analysis for tracking the interested properties of a process. The analysis specification is defined in Flow Logic in order to separate the definition of specification from the actual implementation. Subject to the environment of the hierarchical network, we declare the capability of the attacker of the hierarchical network based on the DolevYao attacker.
The program analysis is fully implemented to compute least estimates for a process. Here we use the Succinct Solver as our constraint solver. It computes the least interpretation of predicate symbols given formulae written in Alternativefree Least Fixed Point logic (ALFP). With this tool, we validate symmetric key protocols applied on hierarchical networks. 
Imprint 
Department of Informatics and Mathematical Modeling, Technical University of Denmark, DTU : DK2800 Kgs. Lyngby, Denmark 
Pages 
149 
Keywords 
Boxed Ambients; Static Analysis; Hardest Attacker; Flow Logic; Hierarchical Network; Cryptographic Protocol 
Fulltext 

Admin 
Creation date: 20060622
Update date: 20121219
Source: dtu
ID: 185885
Original MXD
