The Modelling and Analysis of Security Protocols: the CSP Approach

2.3. Modelling an intruder

If the agent and server processes we created in Section 2.1 were in a world where their messages were transmitted reliably and where there is no other entity generating messages to put into the communication medium, then it seems most unlikely that anything could go wrong. That is not, of course, the world that cryptographic protocols are designed to face. Aside, hopefully, from a different probability of delivery, a better analogy is to imagine Anne and Bob each living on their own desert island, sending messages to each other by putting them in bottles and throwing them into the sea; there is no guarantee of delivery: anyone else might find the bottle and use its contents in any way he can, including putting further ...