Constructing and Reasoning About Security Protocols Using Invariants

In this work we explore the applicability of the programming method of Feijen and van Gasteren to the construction of security protocols. This method addresses the derivation of concurrent programs from a formal specification, and it is based on common notions like invariants and pre- and post-conditions. We show that fundamental security concepts like secrecy and authentication can nicely be specified in this way. Using some small extensions, the style of formal reasoning from this method can be applied to the security domain. To demonstrate our approach, we discuss an authentication protocol and a public-key distribution protocol, and we deal with their composition. Although this work does not contain any new protocols, it does offer a new view on describing, constructing and reasoning about security protocols.