Abstract

Design and veri¯cation of cryptographic protocols has been under investigation for quite sometime. However, most of the attention has been paid for two parties protocols. In group key management and distribution protocols, keys are computed dynamically through cooperation of all protocol participants. Therefore regular approaches for two parties protocols veri¯cation cannot be applied on group key protocols. In this paper, we present a framework for formally verifying of group key management and distribution protocols based on the concept of rank functions. We de¯ne a class of rank functions that satisfy speci¯c requirements and prove the soundness of these rank functions. Based on the set of sound rank functions, we provide a sound and complete inference system to detect attacks in group key management protocols. The inference system provides an elegant and natural proof strategy for such protocols compared to existing approaches. The above formalizations and rank theorems were implemented using the PVS theorem prover. We illustrate our approach by applying the inference system on a generic Di±e-Hellman group protocol and prove it in PVS.