The standard notation consists of a set of principals (traditionally named Alice, Bob, Charlie, and so on) who wish to communicate.
They may have access to a server S, shared keys K, timestamps T, and can generate nonces N for authentication purposes.
A simple example might be the following: This states that Alice intends a message for Bob consisting of a plaintext X encrypted under shared key KA,B.
The notation specifies only the operation and not its semantics — for instance, private key encryption and signature are represented identically.
[4] Several models exist to reason about security protocols in this way, one of which is BAN logic.