Fundamental Ideas II
From Schneider: the precedes relation [Sch98] (called “authenticates” relation in an earlier conference paper)
If S and T are sets of messages,
- S precedes T if a message history with no occurrence of any S cannot contain an occurrence of any T
- I.e., an observation in T implies the prior presence of an S
Used to express authentication: a certain message received by B implies that a prior message (possibly the same message) must have been sent by A
Inductive verification invariant: Suppose a history has no occurrence of S. Then it has no occurrence of T.