Timed traces and strand spaces

Abstract

This paper presents an approach to the analysis of real-time properties of security protocols, based on the Strand Space formalism for describing the behaviour of the participants in the protocol. The approach is compared with a trace-based analysis introduced by Pilegaard et al. [14]. Interval Logic with durations is used to express and reason about temporal phenomena. Strand Spaces were chosen as the starting point for our approach, since the causalities between important events in protocols are revealed in an illustrative manner by this formalism. The advantage of the trace-based approach is that it supports inductive reasoning in connection with the analysis of untimed properties. Interval Logic is chosen as the real-time formalism, as timing requirements and timing properties of security protocols are often expressible as interval properties. As an example, the Kerberos authentication protocol, which is based on concepts like timestamps and lifetimes, and which requires freshness of certain messages, is analysed. © Springer-Verlag Berlin Heidelberg 2007.