Answered

Consider the following authentication protocol given in common syntax:
A, B : Principal
Nb : Nonce
pk : Principal -> Key
1. A->B: {A,B}pk(B)
2. B->A: {B,Nb}pk(A)
3. A->B: {Nb,A}pk(B)
We shall call this protocol PROTOCOL_TWO.

Construct an SPDL specification of PROTOCOL_TWO for verification in Scyther.



Answer :