The language

The sorts we distinguish are $\Principal$, $\Key$, $\Message$and $\Formula$.There are (further unspecified) universes of constants for the sorts $\Principal$ and $\Key$.We view (logical) formulas as being a subsort of the sort of messages, since messages can also consist of nonces, timestamps or other constants, drawn from some further unspecified universe, as well as encrypted messages. So there is an implicit injection $\M :: \Formula \typearrow \Message$.

We use variables $A, B, P, Q, R, \ldots$ for principals, Greek letters $\phi, \psi, \ldots$ for formulas, $M, X, Y, \ldots$ for messages in general, and $K, \ldots$ for keys.

For formulas, the language of the logic has the logical constant $\true$, the logical operators $\land, \lor, \implies$ and $\forall$, and the operator = on the sort $\Message$.Furthermore we have the following operators:

• $\concate :: \Message \times \Message \typearrow \Message$
  (an associative, commutative and idempotent operator for message joining which is an extension of $\land$, the logical-and operator, so that the joining of two messages that happen to be formulas is interpreted as their conjunction)
• $\believes :: \Principal \times \Formula \typearrow \Formula$
• $\oncesaid :: \Principal \times \Message \typearrow \Formula$
  (for messages that have been uttered)
• $\sees :: \Principal \times \Message \typearrow \Formula$
  (for messages that have been received)
• $\possesses :: \Principal \times \Key \typearrow \Formula$
  (possession of information, in our case a key, does not imply any beliefs about validity or usage)
• $\keye :: \Key \times \Principal \times \Principal \typearrow \Formula$
  (symmetric in the last two arguments; intuitively, $\key{P}{Q}{K}$ means that K is a good key between P and Q )
• $\encrypte :: \Key \times \Message \times \Principal \typearrow \Message$
  (for encryption; intuitively, $\encrypt{X}{K}{P}$ denotes X encrypted with K by P )

The ``word'' operators bind more tightly than the traditional logical operators, so that, e.g., $P \believes \phi \:\land\: \psi$ must be interpreted as $(P \believes \phi) \:\land\: \psi$.

In BAN logic $\controls$ and $\fresh$ are primitive operators. We could, equivalently, have introduced these operators as primitives with their definitions turned into axioms.