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.