Beta 1


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, DK-2800 Kgs. Lyngby, Denmark)
Supervisor Nielson, Hanne Riis (Language-Based Technology, Department of Informatics and Mathematical Modeling, Technical University of Denmark, DTU, DK-2800 Kgs. Lyngby, Denmark)
Institution Technical University of Denmark, DTU, DK-2800 Kgs. Lyngby, Denmark
Thesis level Master's thesis
Year 2005
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.
Imprint Department of Informatics and Mathematical Modeling, Technical University of Denmark, DTU : DK-2800 Kgs. Lyngby, Denmark
Pages 149
Keywords Boxed Ambients; Static Analysis; Hardest Attacker; Flow Logic; Hierarchical Network; Cryptographic Protocol
Fulltext
Original PDF imm3977.pdf (0.91 MB)
Admin Creation date: 2006-06-22    Update date: 2012-12-19    Source: dtu    ID: 185885    Original MXD