Automatic security protocol analysis is currently feasible only for small protocols. Since larger protocols quite often are composed of many small protocols, compositional analysis is an attractive, but non-trivial approach. We have developed a framework for compositional analysis of a large class of security protocols. The framework is intended to facilitate automatic as well as manual verification of large structured security protocols. Our approach is to verify properties of component protocols in a multi-protocol environment, then deduce properties about the composed protocol. To reduce the complexity of multi-protocol verification, we introduce a notion of protocol independence and prove a number of theorems that enable analysis of independent component protocols in isolation. To illustrate the applicability of our framework to real-world protocols, we study a key establishment sequence in WiMax consisting of three subprotocols. Except for a small amount of trivial reasoning, the analysis is done using automatic tools.
翻译:自动安全协议分析目前只对小型协议可行。 由于大型协议通常由许多小型协议组成,因此,组成分析是一种吸引人但非三重方法。我们已经制定了对一大批安全协议进行组成分析的框架。该框架旨在便利对大型结构化安全协议进行自动和人工核查。我们的做法是在多议定书环境中核查各组成部分协议的特性,然后对组成协议进行属性推断。为了减少多议定书核查的复杂性,我们引入了协议独立的概念,并证明一些理论可以单独分析独立的部分协议。为了说明我们的框架对现实世界协议的适用性,我们研究了WiMax中由三个子协议组成的一个关键设置序列。除了少量的细微推理之外,分析是使用自动工具进行的。