Static Analysis for Protocol Validation in Hierarchical Networks | Ye Zhang
| | Abstract | The ambient calculus presents a high-level view of mobile computation and gives rise to a high-level 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 Dolev-Yao 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 Alternative-free Least Fixed Point logic (ALFP). With this tool, we validate symmetric key protocols applied on hierarchical networks. | | Keywords | Boxed Ambients, Static Analysis, Hardest Attacker, Flow Logic, Hierarchical Network, Cryptographic Protocol | | Type | Master's thesis [Academic thesis] | | Year | 2005 | | Publisher | Informatics and Mathematical Modelling, Technical University of Denmark, DTU | | Address | Richard Petersens Plads, Building 321, DK-2800 Kgs. Lyngby | | Series | IMM-Thesis-2005-64 | | Note | Supervised by Prof. Hanne Riis Nielson | | Electronic version(s) | [pdf] | | BibTeX data | [bibtex] | | IMM Group(s) | Computer Science & Engineering |
|