Temporal Rank Functions for Forward Secrecy

A number of key establishment protocols claim the property of forward secrecy, where the compromise of a longterm key does not result in the compromise of previously computed session-keys. We describe how such protocols can be modelled using the process algebra CSP and explain why the well-known rank function approach is incapable of proving their correctness. This shortcoming motivates us to propose a generalised proof technique based on the novel concept of a temporal rank function. We apply this approach to two examples: a protocol due to Boyd and the Cliques (AGDH.2) group key agreement protocol.

• Type: Conference
• Year: 2005
• Where: CSFW
• Authors: Rob Delicata, Steve A. Schneider
• Keywords: CSFW 2005, Key Establishment Protocols, Rank Function, Rank Function Approach, Security Privacy