Security protocol notation

Security (engineering) protocol notation is a way of expressing a protocol of correspondance between trusted principles 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...) 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:

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

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