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:
In BAN logic and
are primitive
operators.
We could, equivalently, have introduced these operators as
primitives with their definitions turned into axioms.