The Modelling and Analysis of Security Protocols: the CSP Approach

5.5. Hash functions and Vernam encryption

Hash functions can be used in a Casper script by declaring them as having the type HashFunction in the #Free variables section. If f is declared in this way, then f(m) represents the application of f to message m. For example:

3. a -> b : {f(nb)}{PK(b)}

In such cases, both the sender and the recipient should be able to create f(m); the recipient will only accept a value for this message if the value received matches the value he calculates for himself. It is assumed that all hash functions are known to all agents.

For example, consider the following, somewhat simplified, version of the Needham-Schroeder Signature protocol:

a wants to transmit a message m to b in an authenticated manner; it sends a ...