PROTOCOL Needham-Schroeder-PK2

LOGIC BAN

CONSTANTS

%Principals

A
B
S

%Keys 
%public

V_B
V_A

%Nonces 

N_B
N_A

ASSUMPTIONS
%Messages:
%1.A->B: {A,N_A}_{V_B}
sees(B,encrypt(N_A,V_B))

%2.B->A: {N_A,N_B}_{V_A}
sees(A,encrypt(combine(secret(A,B,N_B),N_A),V_A))

%3.A->B: {N_B}_{V_B}
sees(B,encrypt(combine(pair(secret(A,B,N_A),believes(B,secret(A,B,N_B))),N_B),V_B))

%initial beliefs

believes(B,publickey(V_B,B))
believes(A,publickey(V_A,A))
believes(A,fresh(N_A))
believes(B,fresh(N_B))
believes(A,secret(A,B,N_A))
believes(B,secret(A,B,N_B))


GOALS


believes(A,believes(B,secret(A,B,N_B)))
believes(B,believes(A,secret(A,B,N_A)))
believes(B,believes(A,believes(B,secret(A,B,N_B))))