The Modelling and Analysis of Security Protocols: the CSP Approach

Notation in protocol descriptions

Lower case is used for variables: message components and keys that are generated in a particular run (e.g. nonces, session keys). Lower case is also used for agent names in the general description of the run. e.g. k_ab for a session key generated in that run.

Upper case is used for constants: items that are fixed for all runs (e.g. long-term session keys, the name of the server, public and secret agent keys). So PK_a for a’s public key, SK_a for a’s secret key, PK_J for Jeeves’ public key (since the functions PK and SK from agents’ names to keys are constant). If K is upper case then the key is fixed prior to communication, e.g. K_AB. If it is lower case, e.g. k_ab then it is a key being set up by the protocol under ...