...holds

Rules without side condition will be presented as follows: $\mbox{$\frac{\displaystyle {\mbox{$p_1\ldots p_n$}}}{\displaystyle {m} } $}$

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

...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.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.