...holds
Rules without side condition will be presented as follows:
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

...freshness
The symbol Fresh denotes a unary predicate that holds whenever its argument is fresh.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

...role
Actually, the verification involves only those roles that require identity proofs from other roles. In the case of the Woo and Lam protocol, only the role B is involved in the verification since the protocol deals with unidirectional authentication. In a bidirectional authentication protocol, the two principals are involved.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.