On the semantics of Alice&Bob specifications of security protocols

In the context of security protocols, the so-called Alice&Bob notation is often used to describe the messages exchanged between honest principals in successful protocol runs. While intuitive, this notation is ambiguous in its description of the actions taken by principals, in particular with respect to the conditions they must check when executing their roles and the actions they must take when the checks fail. In this paper, we investigate the semantics of protocol specifications in Alice&Bob notation. We provide both a denotational and an operational semantics for such specifications, rigorously accounting for these conditions and actions. Our denotational semantics is based on a notion of incremental symbolic runs, which reflect the data possessed by principals and how this data increases monotonically during protocol execution. We contrast this with a standard formalization of the behavior of principals, which directly interprets message exchanges as sequences of atomic actions. In particular, we provide a complete characterization of the situations where this simpler, direct approach is adequate and prove that incremental symbolic runs are more expressive in general. Our operational semantics, which is guided by the denotational semantics, implements each role of the specified protocol as a sequential process of the pattern-matching spi calculus.