saag-1----Page:10
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27
|
Basic Roles role Basic_Role (…) played_by … def= owns {?: T} local {e} init Init accepts Accept transition event1 ? action1 event2 ? action2 … end role role Alice (A, B: agent, Ka, Kb: public_key, SND, RCV: channel (dy)) played_by A def= local State:nat, Na:text (fresh), Nb:text init State = 0 transition 1. State =0 /\ RCV(start) =|> State'=2 /\ SND({Na'.A}_Kb) /\ witness(A,B,na,Na') 2. State =2 /\ RCV({Na.Nb'}_Ka) =|> State'=4 /\ SND({Nb'}_Kb) /\ request(A,B,nb,Nb') /\ secret(Na,B) end role General Pattern Initiator Role in NSPK |