6.3. Wiring the network together

The legitimate principals of the system are coded so that all of their interactions with the rest of the system are programmed using channels input and output:

ALL_PRINCIPALS = Union({Agent, Server}) 

channel input : ALL_PRINCIPALS.ALL_PRINCIPALS.INPUT_INT_MSG_BODY 
channel output : ALL_PRINCIPALS.ALL_PRINCIPALS.OUTPUT_INT_MSG_BODY

The first index represents the purported sender of the message, and the second the intended receiver, and the data components are the union of the unfactored message-body tuples discussed above.

Rather than simply wire these channels point-to-point between the principals, the parallel composition of the system needs to allow for the potential actions of the intruder. This is mediated ...

Get The Modelling and Analysis of Security Protocols: the CSP Approach now with the O’Reilly learning platform.

O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.

Start your free trial