Rank Theorems for Forward Secrecy in Group Key Management Protocols

Design and verification of cryptographic protocols has been under investigation for quite sometime. However, little has been done for the class of protocols that deals with group key management and distribution, and have special security properties, such as forward secrecy. In this paper, we define a formal model and establish rank theorems for forward properties based on a set of generic formal specification requirements for group key management and distribution protocols. Rank theorems imply the validity of the security property to be proved, and are deducted from a set of rank functions we define over the protocol. The above formalizations and rank theorems were implemented using the PVS theorem prover. We illustrate our approach on the verification of forward secrecy for the Enclaves protocol designed at SRI.