agents: A, B types: N:nonce init Aknows(kA), A'knows(KA), A'knows(KB), B'knows(KA) Bknows(kB), B'knows(KB) ((N)k)K =((N)K)k= N A'claim(A) B'claim(B) step0 A'knows(NA)^message((NA)KB)->B'knows((NA)KB) step1 message((NA)KA) -> A'knows(B'knows(NA)) step2 A'knows(B'knows(NA)) -> A'knows(B'knows(kB)) SUCCESS: A'knows(B'=B)