Next: Soundness Up: A semantics for BAN Previous: The model

# Semantics of formulas

We define the relation between states and formulas (where means: in state s formula holds) inductively on the structure of formulas as the least relation satisfying:

The notation above means: with u substituted for the free occurrences of x . If , the whole formula may be substituted for , and since , the recursion'' in the definition of is unbounded, whence the appeal above to least relation''.

Note that the relation is not monotonic in its left argument, i.e., when , does in general not imply .