PROTOCOL Andrew-RPC2

LOGIC BAN

CONSTANTS

%Principals

A
B

%Keys

K_{AB}
K'_{AB}

%Nonces

N_A
N_B
N'_B



ASSUMPTIONS

%Messages
%1.A->B: A,{N_A}_{K_AB}
sees(B,encrypt(N_A,K_{AB}))

%2.B->A: {N_A+1,N_B}_{K_AB}
sees(A,encrypt(pair(N_A,N_B),K_{AB}))

%3.A->B:{N_B+1}_{K_{AB}}
sees(B,encrypt(N_B,K_{AB}))

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

%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(N_B))
believes(B, fresh(N_B))
believes(B, fresh(N'_B))

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})))