Validating security protocols is a well-known hard problem even in a simple setting of a single global network. But a real network often consists of, besides the public-accessed part, several sub-networks and thereby forms a hierarchical structure. In this paper we first present a process calculus capturing the characteristics of hierarchical networks and describe the behavior of protocols on such networks. We then develop a static analysis to automate the validation. Finally we demonstrate how the technique can benefit the protocol development and the design of network systems by presenting a series of experiments we have conducted.
|Title of host publication||Automated Technology For Verification and Analysis, Proceedings|
|Place of Publication||Berlin|
|Publication status||Published - 2006|
|Series||Lecture Notes in Computer Science|