PROTOCOL Andrew-RPC3

LOGIC BAN3

CONSTANTS

%Principals

A
B

%Keys

K_{AB}
K'_{AB}

%Nonces

N_A



ASSUMPTIONS

%Messages
%1.A->B: A,N_A
%2.B->A: {N_A,K'_AB}_{K_AB}
sees(A,encrypt(pair(sharedkey(A, B,K'_{AB}),N_A),K_{AB}))

%3.A->B:{N_A}_{K'_{AB}}
sees(B,encrypt(sharedkey(A,B,K'_{AB}),K'_{AB}))

%4.B->A:N'_B 


%initial beliefs

believes(A, sharedkey(A, B,K_{AB}))
believes(B, sharedkey(A, B,K_{AB}))
believes(A, jurisdiction(B, sharedkey( A, B,K'_{AB})))
believes(B, sharedkey(A, B,K'_{AB}))
believes(A, fresh(N_A))
believes(B,fresh(K'_{AB}))



GOALS

believes(B,sharedkey(A, B,K'_{AB}))
believes(A,sharedkey(A, B,K'_{AB}))
believes(A,believes(B,sharedkey(A, B,K'_{AB})))
believes(B,believes(A,sharedkey(A, B,K'_{AB})))