Security protocol notation

Security (engineering) protocol notation is a way of expressing a protocol of correspondance between entities of a dynamic system, such as a computer network. It allows reasoning about the properties of such a system, and provides a formal model, to which the BAN logic can be applied.

The standard notation consists of a set of individuals (traditionally named Alice, Bob, Charlie and so on) who wish to communicate. They may have access to shared keys K, timestamps T, and can generate nonces for authentication purposes.

A simple example might be the following:

$A\rightarrow B:\{X\}_{K_{AB}}$

This states that Alice intends a message for Bob consisting of a plain text X encrypted under shared key K_AB.

A key with two subscripts is a symmetric key shared by the two corresponding individuals. A key with one subscript is the public key of the corresponding individual. A private key is represented as the inverse of the public key.

The notation specifies only the operation and not its semantics - for instance, public key encryption and signature are represented identically.

We can express more complicated protocols in such a fashion, see Kerberos as an example.