The Modelling and Analysis of Security Protocols: the CSP Approach

2.1. Trustworthy processes

The typical security protocol involves several agents (often two: an initiator and a responder) and perhaps a server that performs some service such as key generation, translation or certification. We will see how to program processes that faithfully run the functions of a protocol in an entirely correct and trustworthy way, before worrying about how we are going to look for security flaws.

If we look at the Yahalom protocol:

it is clear that a trustworthy agent can take one of two roles, namely as initiator (the sender of message 1, designated a above), or responder (the sender of message 2, designated b). It would ...