Protocol Amended_Needham_Schroeder_Shared_Key_Protocol: A>InitiatorANS(B:Id, kAT:sym-key(A, T)):= out(A). in(x). new(nA). out(A, B, nA, x). in(xT). 1: decrypt xT as {nA, B, kAB, xB}_kAT. out(xB). in(yB). 2: decrypt yB as {y}_kAB. commit(A, B). run(A, B). new(prec_y). 3: encrypt {prec_y}_kAB as z. out(z). 0 B>ResponderANS(A:Id, kBT:sym-key(B, T)):= in(A). new(nB). 4: encrypt {A, nB}_kBT as x. out(x). in(xT). 5: decrypt xT as {nB, A, kAB}_kBT. new(a). run(B, A). 2: encrypt {a}_kAB as y. out(y). in(zA). 3: decrypt zA as {prec_a}_kAB. commit(B, A). 0 T>ServerANS(A:Id, kAT:sym-key(A, T), B:Id, kBT:sym-key(B, T)):= in(A, B, xA, x). 4: decrypt x as {A, xB}_kBT. new(kAB). 5: encrypt {xB, A, kAB}_kBT as yB. 1: encrypt {xA, B, kAB, yB}_kAT as y. out(y). 0 start. let kAT = sym-key(A, T). let kBT = sym-key(B, T). (A>InitiatorANS(B, kAT) | B>ResponderANS(A, kBT) | T>ServerANS(A, kAT, B, kBT))