Abstract
A number of cryptographic protocols have appeared in the literature that claim to provide forward secrecy. The idea of forward secrecy is that if a long-term key is compromised then any session-keys that were previously established using the long-term key should remain secret. Forward secrecy is important in scenarios where session-keys need protection beyond the time-span during which they are used. These situations typically arise when session-keys are used for data encryption, rather than just authentication. There appears to be a disparity between the growing number of protocols that claim forward secrecy, and the work carried out on its formal analysis. In contrast to secrecy and authentication, the formal verification of forward secrecy has, with some exceptions received little attention in the literature. This paper fills the gap for the rank function approach.