Operators

The model makes use of three main operators that extend a given set of messages H. They are defined inductively, and enjoy several laws.

parts H

is built from H by repeatedly adding the components of compound messages and the bodies of encrypted messages. Intuitively, it formalises all the knowledge that can be obtained from H, except for the keys that encrypt messages in H.

analz H

is built from H by repeatedly adding the components of compound messages and the bodies of messages encrypted under keys already in analz H. It is a subset of parts H because it doesn't break ciphers.

synth H

models the messages that the spy can built up from elements of H, including agent names, timestamps, compound messages, and messages encrypted with keys in H. Agent names are included because they are publicly known, timestamps because they can sometimes be guessed

Another operator models the set of messages an agent A receives from a trace evs: sees A evs.

It is inductively defined assuming that honest agents see only the messages intended for themselves, while the spy sees all traffic. Therefore, the set synth(analz(sees Spy evs))

denotes all the fraudulent messages the spy can send by observing the trace evs. A spy able to send such a large number of messages has a potentially infinite behaviour [8] which goes beyond the limits of formalisations by state-enumeration methods.