Constructs

P bel X P believes X

P sees X P received X in a message

P said X P once said X

P controls X P has jurisdiction over X

fresh(X) X has not been used before

P <-K-> Q P and Q may use key K for private communication

K-> P P has K as public key

P <-X-> Q X is a secret shared by P and Q

{X}K X encrypted under K

Y X combined with Y

K-1 inverse key to K

(This symbolism is not quite standard)