Timed Models for Protocol Security

The notion of time is prerequisite for describing and verifying the security properties of key management protocols. Without it, properties relating to the expiration of keys and the freshness of messages and nonces cannot be formulated. Recently Burrows, Abadi and Needham proposed a formal system for protocol verification which includes an ability to reason about time. In essence their "Logic of Authentication" is a proof theory for reasoning about key management protocols. One difficulty with such a logic lies in justifying the inferences that can be made. We approach this problem by developing an accompanying model theory for protocol security. Model theoretic techniques have been used before in the protocol verification literature, but our approach is different in two respects. First we consider a model theory which includes a notion of time. Second, the purpose of much of the previous model theoretic work was aimed at developing protocol verification tools and so assumptions abou..