Next: Axiomatisation Up: The logic Previous: The logic

## The language

The sorts we distinguish are , , and .There are (further unspecified) universes of constants for the sorts and .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 .

We use variables for principals, Greek letters for formulas, for messages in general, and for keys.

For formulas, the language of the logic has the logical constant , the logical operators and , and the operator = on the sort .Furthermore we have the following operators:

• (an associative, commutative and idempotent operator for message joining which is an extension of , the logical-and operator, so that the joining of two messages that happen to be formulas is interpreted as their conjunction)

• (for messages that have been uttered)

• (for messages that have been received)

• (possession of information, in our case a key, does not imply any beliefs about validity or usage)

• (symmetric in the last two arguments; intuitively, means that K is a good key between P and Q )

• (for encryption; intuitively, denotes X encrypted with K by P )
The word'' operators bind more tightly than the traditional logical operators, so that, e.g., must be interpreted as .

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

Next: Axiomatisation Up: The logic Previous: The logic