PROTOCOL X509

LOGIC BAN

CONSTANTS

%Principals

A
B

%Keys 

%private
S_B
S_A

%public

V_B
V_A

%Nonces

N_A
N_B

%Timestamps

T_A
T_B

%data
X_A
X_B
Y_A
Y_B

ASSUMPTIONS
%Messages:
%1.A->B: A,{T_A,N_A,B,X_A,{Y_A}_V_B}_{S_A}
sees(B,encrypt(pair(T_A,pair(X_A,pair(N_A,encrypt(Y_A,V_B)))),S_A))

%2.B->A: B,{T_B,N_B,A,N_A,X_B,{Y_B}_V_A}_{S_B}
sees(A,encrypt(pair(T_B,pair(N_B,pair(N_A,pair(X_B,encrypt(Y_B,V_A))))),S_B))

%2.A->B: A,{N_B}_{S_A}
sees(B,encrypt(N_B,S_A))

%initial beliefs

believes(A,publickey(V_A,A))
believes(A,publickey(V_B,B))
believes(B,publickey(V_B,B))
believes(B,publickey(V_A,A))
believes(A,fresh(N_A))
believes(B,fresh(N_B))
believes(B,fresh(T_A))
believes(A,fresh(T_B))
inv(V_B,S_B)
inv(V_A,S_A)


GOALS

believes(B, believes(A,X_A))
believes(A, believes(B,X_B))
believes(A, believes(B, Y_B))

