
PROTOCOL Nesset

LOGIC BAN

CONSTANTS

A
B
N_A
N_B
K_{AB}
S_A
V_A

ASSUMPTIONS

sees(B,encrypt(pair(N_A,sharedkey(A,B,K_{AB})),S_A))
sees(A,encrypt(sharedkey(A,B,K_{AB}),K_{AB}) )

inv(V_A,S_A)

believes(B,publickey(V_A,A))
believes(B,fresh(N_A))
believes(A,sharedkey(A,B,K_{AB}))
believes(A,fresh(sharedkey(A,B,K_{AB})))
believes(B,jurisdiction(A,sharedkey(A,B,K_{AB})))


GOALS

believes(B,sharedkey(A,B,K_{AB}))
believes(A,believes(B,sharedkey(A,B,K_{AB})))


