PROTOCOL challenge1

LOGIC AUTLOG

CONSTANTS

A
B
K_{AB}
R_B

ASSUMPTIONS

believes(B,fresh(R_B))
believes(B,secret(A,B,R_B))

sees(A,encrypt(secret(A,B,R_B),K_{AB}))
sees(B,combine(R_B,R_B))


GOALS

believes(B,says(A,R_B))
believes(A, said(B, secret( A, B,R_B)))