PROTOCOL Wide-mouthed-frog

LOGIC BAN

CONSTANTS

%Principals

A 
B
S

%Keys

K_{AS}
K_{AB}
K_{BS}

%Timestamps

T_S
T_A

ASSUMPTIONS

%Messages
%1.A->S: A,{T_A,B,K_AB}_{K_AS}
sees(S,encrypt(pair(T_A,sharedkey(A,B,K_{AB})),K_{AS}))

%2.S->B: {T_S,A,K_AB}_{K_BS}

sees(B,encrypt(pair(T_S,believes(A,sharedkey(A,B,K_{AB}))),K_{BS}))

%initial believes

believes(A,sharedkey(A,S,K_{AS}))
believes(B,sharedkey(B,S,K_{BS}))
believes(S,sharedkey(A,S,K_{AS}))
believes(S,sharedkey(B,S,K_{BS}))
believes(A,sharedkey(A,B,K_{AB}))
believes(S,fresh(T_A))
believes(B,fresh(T_S))
believes(B,jurisdiction(A,sharedkey(A,B,K_{AB})))
believes(B,jurisdiction(S,believes(A,sharedkey(A,B,K_{AB}))))

GOALS


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