Rank Functions Based Inference System for Group Key Management Protocols Verification
Amjad Gawanmeh, Adel Bouhoula, Sofl μ ene Tahar · Spectrum Research Repository (Concordia University) · 2009
Design and verification of cryptographic protocols has been under inves-tigation for quite sometime. However, most of the attention has been paid for two parties protocols. In group key management and distribution pro-tocols, keys are computed dynamically through cooperation of all protocol participants. Therefore regular approaches for two parties protocols verifi-cation cannot be applied on group key protocols. In this paper, we present a framework for formally verifying of group key management and distribu-tion protocols based on the concept of rank functions. We define a class of rank functions that satisfy specific 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 manage-ment protocols. The inference system provides an elegant and natural proof strategy for such protocols compared to existing approaches. The above for-malizations and rank theorems were implemented using the PVS theorem prover. We illustrate our approach by applying the inference system on a generic Diffie-Hellman group protocol and prove it in PVS. 1