**************************************************************************** *** OBJECT LEVEL REPRESENTATION *** cf2Obj1Comm defines a situation with two agents: Alice and Bob. *** Alice initiates a communication with Bob. **************************************************************************** (down NSPK : red meta-rewrite(NSPK, up(NSPK,cf2Obj2Comm), 0) .) Result Configuration : boundary ( < alice : NSPKAgent | cnt : 3 , dcom : mtfset , roler : mtrun , rolei : mtrun , seckey : skalice , ecom : ecom+ (ecom(i,n(alice,1),bob,n(bob,1)), ecom(r,n(alice,2),bob,n(bob,2))) > < bob : NSPKAgent | cnt : 3 , dcom : mtfset , roler : mtrun , rolei : mtrun , seckey : skbob , ecom : ecom+ (ecom(i,n(bob,2),alice,n(alice,2)), ecom(r,n(bob,1),alice,n(alice,1))) > ) **************************************************************************** *** META LEVEL REPRESENTATION *** cf2Obj1Comm defines a situation with two agents: Alice and Bob. *** Alice initiates a communication with Bob. **************************************************************************** (red meta-rewrite(NSPK, {'cf2Obj1Comm}'Configuration, 0) .) Reduce in SEARCH : meta-rewrite ( NSPK , { 'cf2Obj1Comm } 'Configuration , 0 ) . Result Term : 'boundary['__ ['<_:_|_>[{ 'alice} 'Principal,{'NSPKAgent}'NSPKAgent, '_`,_['cnt`:_[{'2}'NzMachineInt], 'dcom`:_[{'mtfset}'FieldSet], 'roler`:_[{'mtrun}'Run], 'rolei`:_[{'mtrun}'Run], 'seckey`:_[{'skalice}'PKey], 'ecom`:_['ecom[{'i}'Role, 'n[{'alice}'Principal,{'1}'NzMachineInt], {'bob}'Principal, 'n[{'bob}'Principal,{'1}'NzMachineInt]]]]], '<_:_|_>[{'bob}'Principal,{'NSPKAgent}'NSPKAgent, '_`,_ ['cnt`:_[{'2}'NzMachineInt], 'dcom`:_[{'mtfield}'Field], 'roler`:_[{'mtrun}'Run], 'rolei`:_[{'mtrun}'Run], 'seckey`:_[{'skbob}'PKey], 'ecom`:_['ecom[{'r}'Role, 'n[{'bob}'Principal,{'1}'NzMachineInt], {'alice}'Principal, 'n[{'alice}'Principal,{'1}'NzMachineInt]]]]]]] **************************************************************************** *** Given a scenario with 2 agents and 1 Intruder *** The following rewrite term searches for an attack starting *** from the initial configuration (cf2Agents1Intruder) using *** the listed rules (IntruderRecognizeAttack ... IntruderOverhearMessage3) *** stopping as soon as the rule "IntruderRecognizeAttack" could be applied. *** The maximal depth of the search tree is 11. *** This search delivers the attack found by Gavin Lowe **************************************************************************** (red boundedDepthFirstSearchUntilStopRules( NSPK, {'cf2Agents1Intruder}'Configuration, ('IntruderRecognizeAttack 'BeginRun 'Message1Rec 'Message2Rec 'Message3Rec 'IntruderAcceptEveryMessage1 'IntruderAcceptEveryMessage2 'IntruderAcceptEveryMessage3 'IntruderInterceptMessage1 'IntruderInterceptMessage2 'IntruderInterceptMessage3 'IntruderFakeMessage1 'IntruderFakeMessage2 'IntruderFakeMessage3 'IntruderReplayMessage 'IntruderOverhearMessage1 'IntruderOverhearMessage2 'IntruderOverhearMessage3), 'IntruderRecognizeAttack, 11) .) Reduce in SEARCH : boundedDepthFirstSearchUntilStopRules ( NSPK , {'cf2Agents1Intruder } 'Configuration , 'IntruderRecognizeAttack 'BeginRun 'Message1Rec 'Message2Rec 'Message3Rec 'IntruderAcceptEveryMessage1 'IntruderAcceptEveryMessage2 'IntruderAcceptEveryMessage3 'IntruderInterceptMessage1 'IntruderInterceptMessage2 'IntruderInterceptMessage3 'IntruderFakeMessage1 'IntruderFakeMessage2 'IntruderFakeMessage3 'IntruderReplayMessage 'IntruderOverhearMessage1 'IntruderOverhearMessage2 'IntruderOverhearMessage3 , 'IntruderRecognizeAttack, 11) . Result Strategy : stop(11,path(path(path(path(path(path(path(path(path(path(path( {'cf2Agents1Intruder}'Configuration, step( 'BeginRun, 0, 'boundary['__[ '<_:_|_>[{'alice}'Principal,{'NSPKAgent}'NSPKAgent, '_`,_['cnt`:_[{'2}'NzMachineInt], 'dcom`:_[{'mtfset}'FieldSet], 'roler`:_[{'mtrun}'Run], 'rolei`:_['run+[{'mtrun}'Run, 'run['n[{'alice}'Principal,{'1}'NzMachineInt], {'mrx}'Principal, {'mtfield}'Field]]], 'seckey`:_[{'skalice}'PKey], 'ecom`:_[{'mtecom}'EstabCom]]], '<_:_|_>[{'bob}'Principal,{'NSPKAgent}'NSPKAgent, '_`,_['cnt`:_[{'1}'NzMachineInt], 'dcom`:_[{'mtfield}'Field], 'roler`:_[{'mtrun}'Run], 'rolei`:_[{'mtrun}'Run], 'seckey`:_[{'skbob}'PKey], 'ecom`:_[{'mtecom}'EstabCom]]], '<_:_|_>[{'mrx}'Principal,{'Intruder}'Intruder, '_`,_['cnt`:_[{'1}'NzMachineInt], 'dcom`:_[{'mtfield}'Field], 'roler`:_[{'mtrun} 'Run], 'rolei`:_[{'mtrun}'Run], 'seckey`:_[{'skmrx}'PKey], 'ecom`:_[{'mtecom}'EstabCom], 'agents`:_['fset+[{'bob} 'Principal,{'mrx}'Principal]], 'msgs`:_[{'mtfset}'FieldSet], 'ncs`:_[{'mtfset}'FieldSet]]], 'msg[{'alice}'Principal, {'mrx}'Principal, 'ped[{'pkmrx}'PKey,'tuple['n[{'alice} 'Principal,{'1}'NzMachineInt], {'alice}'Principal]]]]])), step( 'IntruderAcceptEveryMessage1, 0, 'boundary['__[ '<_:_|_>[{'alice}'Principal,{'NSPKAgent}'NSPKAgent, '_`,_['cnt`:_[{'2}'NzMachineInt], 'dcom`:_[{'mtfset}'FieldSet], 'roler`:_[{'mtrun}'Run], 'rolei`:_['run+[{'mtrun}'Run, 'run['n[{'alice}'Principal,{'1}'NzMachineInt], {'mrx}'Principal, {'mtfield}'Field]]], 'seckey`:_[{'skalice}'PKey], 'ecom`:_[{'mtecom}'EstabCom]]], '<_:_|_>[{'bob}'Principal,{'NSPKAgent}'NSPKAgent, '_`,_['cnt`:_[{'1}'NzMachineInt], 'dcom`:_[{'mtfield}'Field], 'roler`:_[{'mtrun}'Run], 'rolei`:_[{'mtrun}'Run], 'seckey`:_[{'skbob}'PKey], 'ecom`:_[{'mtecom}'EstabCom]]], '<_:_|_>[{'mrx}'Principal,{'Intruder}'Intruder, '_`,_['cnt`:_[{'1}'NzMachineInt], 'dcom`:_[{'mtfield}'Field], 'roler`:_[{'mtrun}'Run], 'rolei`:_[{'mtrun}'Run], 'seckey`:_[{'skmrx}'PKey], 'ecom`:_[{'mtecom}'EstabCom], 'agents`:_['fset+[{'alice}'Principal, {'bob}'Principal, {'mrx}'Principal]], 'msgs`:_[{'mtfset}'FieldSet], 'ncs`:_['fset+[{'mtfset}'FieldSet, 'n[{'alice}'Principal,{'1}'NzMachineInt]]]]]]])), step( 'IntruderFakeMessage1, 0, 'boundary['__[ '<_:_|_>[{'alice}'Principal,{'NSPKAgent}'NSPKAgent, '_`,_['cnt`:_[{'2}'NzMachineInt], 'dcom`:_[{'mtfset}'FieldSet], 'roler`:_[{'mtrun}'Run], 'rolei`:_['run+[{'mtrun}'Run, 'run['n[{'alice}'Principal,{'1}'NzMachineInt], {'mrx}'Principal, {'mtfield}'Field]]], 'seckey`:_[{'skalice}'PKey], 'ecom`:_[{'mtecom}'EstabCom]]], '<_:_|_>[{'bob}'Principal,{'NSPKAgent}'NSPKAgent, '_`,_['cnt`:_[{'1}'NzMachineInt], 'dcom`:_[{'mtfield}'Field], 'roler`:_[{'mtrun}'Run], 'rolei`:_[{'mtrun}'Run], 'seckey`:_[{'skbob}'PKey], 'ecom`:_[{'mtecom}'EstabCom]]], '<_:_|_>[{'mrx}'Principal,{'Intruder}'Intruder, '_`,_['cnt`:_[{'1}'NzMachineInt], 'dcom`:_[{'mtfield}'Field], 'roler`:_[{'mtrun}'Run], 'rolei`:_[{'mtrun}'Run], 'seckey`:_[{'skmrx}'PKey], 'ecom`:_[{'mtecom}'EstabCom], 'agents`:_['fset+[{'alice}'Principal, {'bob}'Principal, {'mrx}'Principal]], 'msgs`:_[{'mtfset}'FieldSet], 'ncs`:_['fset+[{'mtfset}'FieldSet, 'n[{'alice}'Principal,{'1}'NzMachineInt]]]]], 'msg[{'alice}'Principal, {'bob}'Principal, 'ped[{'pkbob}'PKey,'tuple['n[{'alice}'Principal,{'1}'NzMachineInt], {'alice}'Principal]]]]])), step( 'Message1Rec, 0, 'boundary['__[ '<_:_|_>[{'alice}'Principal,{'NSPKAgent}'NSPKAgent, '_`,_['cnt`:_[{'2}'NzMachineInt], 'dcom`:_[{'mtfset}'FieldSet], 'roler`:_[{'mtrun}'Run], 'rolei`:_['run+[{'mtrun}'Run, 'run['n[{'alice}'Principal,{'1}'NzMachineInt], {'mrx}'Principal, {'mtfield}'Field]]], 'seckey`:_[{'skalice}'PKey], 'ecom`:_[{'mtecom}'EstabCom]]], '<_:_|_>[{'bob}'Principal,{'NSPKAgent}'NSPKAgent, '_`,_['cnt`:_[{'2}'NzMachineInt], 'dcom`:_[{'mtfield}'Field], 'roler`:_['run+[{'mtrun}'Run, 'run['n[{'bob}'Principal,{'1}'NzMachineInt], {'alice}'Principal, 'n[{'alice}'Principal,{'1}'NzMachineInt]]]], 'rolei`:_[{'mtrun}'Run], 'seckey`:_[{'skbob}'PKey], 'ecom`:_[{'mtecom}'EstabCom]]], '<_:_|_>[{'mrx}'Principal,{'Intruder}'Intruder, '_`,_['cnt`:_[{'1}'NzMachineInt], 'dcom`:_[{'mtfield}'Field], 'roler`:_[{'mtrun}'Run], 'rolei`:_[{'mtrun}'Run], 'seckey`:_[{'skmrx}'PKey], 'ecom`:_[{'mtecom}'EstabCom], 'agents`:_['fset+[{'alice}'Principal, {'bob}'Principal, {'mrx}'Principal]], 'msgs`:_[{'mtfset}'FieldSet], 'ncs`:_['fset+[{'mtfset}'FieldSet, 'n[{'alice}'Principal,{'1}'NzMachineInt]]]]], 'msg[{'bob}'Principal, {'alice}'Principal, 'ped[{'pkalice}'PKey,'cat['n[{'alice}'Principal,{'1}'NzMachineInt], 'n[{'bob}'Principal,{'1}'NzMachineInt]]]]]])), step( 'IntruderInterceptMessage2, 0, 'boundary['__[ '<_:_|_>[{'alice}'Principal,{'NSPKAgent}'NSPKAgent, '_`,_['cnt`:_[{'2}'NzMachineInt], 'dcom`:_[{'mtfset}'FieldSet], 'roler`:_[{'mtrun}'Run], 'rolei`:_['run+[{'mtrun}'Run, 'run['n[{'alice}'Principal,{'1}'NzMachineInt],XS {'mrx}'Principal, {'mtfield}'Field]]], 'seckey`:_[{'skalice}'PKey], 'ecom`:_[{'mtecom}'EstabCom]]], '<_:_|_>[{'bob}'Principal,{'NSPKAgent}'NSPKAgent, '_`,_['cnt`:_[{'2}'NzMachineInt], 'dcom`:_[{'mtfield}'Field], 'roler`:_['run+[{'mtrun}'Run, 'run['n[{'bob}'Principal,{'1}'NzMachineInt], {'alice}'Principal, 'n[{'alice}'Principal,{'1}'NzMachineInt]]]], 'rolei`:_[{'mtrun}'Run], 'seckey`:_[{'skbob}'PKey], 'ecom`:_[{'mtecom}'EstabCom]]], '<_:_|_>[{'mrx}'Principal,{'Intruder}'Intruder, '_`,_['cnt`:_[{'1}'NzMachineInt], 'dcom`:_[{'mtfield}'Field], 'roler`:_[{'mtrun}'Run], 'rolei`:_[{'mtrun}'Run], 'seckey`:_[{'skmrx}'PKey], 'ecom`:_[{'mtecom}'EstabCom], 'agents`:_['fset+[{'alice}'Principal, {'bob}'Principal, {'mrx}'Principal]], 'msgs`:_['fset+[{'mtfset}'FieldSet, 'ped[{'pkalice}'PKey, 'cat['n[{'alice}'Principal,{'1}'NzMachineInt], 'n[{'bob}'Principal,{'1}'NzMachineInt]]]]], 'ncs`:_['fset+[{'mtfset}'FieldSet, 'n[{'alice}'Principal,{'1}'NzMachineInt]]]]]]])), step( 'IntruderReplayMessage, 1, 'boundary['__[ '<_:_|_>[{'alice}'Principal,{'NSPKAgent}'NSPKAgent, '_`,_['cnt`:_[{'2}'NzMachineInt], 'dcom`:_[{'mtfset}'FieldSet], 'roler`:_[{'mtrun}'Run], 'rolei`:_['run+[{'mtrun}'Run, 'run['n[{'alice}'Principal,{'1}'NzMachineInt], {'mrx}'Principal, {'mtfield}'Field]]], 'seckey`:_[{'skalice}'PKey], 'ecom`:_[{'mtecom}'EstabCom]]], '<_:_|_>[{'bob}'Principal,{'NSPKAgent}'NSPKAgent, '_`,_['cnt`:_[{'2}'NzMachineInt], 'dcom`:_[{'mtfield}'Field], 'roler`:_['run+[{'mtrun}'Run, 'run['n[{'bob}'Principal,{'1}'NzMachineInt], {'alice}'Principal, 'n[{'alice}'Principal,{'1}'NzMachineInt]]]], 'rolei`:_[{'mtrun}'Run], 'seckey`:_[{'skbob}'PKey], 'ecom`:_[{'mtecom}'EstabCom]]], '<_:_|_>[{'mrx}'Principal,{'Intruder}'Intruder, '_`,_['cnt`:_[{'1}'NzMachineInt], 'dcom`:_[{'mtfield}'Field], 'roler`:_[{'mtrun}'Run], 'rolei`:_[{'mtrun}'Run], 'seckey`:_[{'skmrx}'PKey], 'ecom`:_[{'mtecom}'EstabCom], 'agents`:_['fset+[{'alice}'Principal, {'bob}'Principal, {'mrx}'Principal]], 'msgs`:_['fset+[{'mtfset}'FieldSet, 'ped[{'pkalice}'PKey, 'cat['n[{'alice}'Principal,{'1}'NzMachineInt], 'n[{'bob}'Principal,{'1}'NzMachineInt]]]]], 'ncs`:_['fset+[{'mtfset}'FieldSet, 'n[{'alice}'Principal,{'1}'NzMachineInt]]]]], 'msg[{'mrx}'Principal, {'alice}'Principal, 'ped[{'pkalice}'PKey,'cat['n[{'alice}'Principal,{'1}'NzMachineInt], 'n[{'bob}'Principal,{'1}'NzMachineInt]]]]]])), step( 'Message2Rec, 0, 'boundary['__[ '<_:_|_>[{'alice}'Principal,{'NSPKAgent}'NSPKAgent, '_`,_['cnt`:_[{'2}'NzMachineInt], 'dcom`:_[{'mtfset}'FieldSet], 'roler`:_[{'mtrun}'Run], 'rolei`:_[{'mtrun}'Run], 'seckey`:_[{'skalice}'PKey], 'ecom`:_['ecom[{'i} 'role,'n[{'alice}'Principal,{'1}'NzMachineInt], {'mrx}'Principal, 'n[{'bob}'Principal,{'1}'NzMachineInt]]]]], '<_:_|_>[{'bob}'Principal,{'NSPKAgent}'NSPKAgent, '_`,_['cnt`:_[{'2}'NzMachineInt], 'dcom`:_[{'mtfield}'Field], 'roler`:_['run+[{'mtrun}'Run, 'run['n[{'bob}'Principal,{'1}'NzMachineInt], {'alice}'Principal, 'n[{'alice}'Principal,{'1}'NzMachineInt]]]], 'rolei`:_[{'mtrun}'Run], 'seckey`:_[{'skbob}'PKey], 'ecom`:_[{'mtecom}'EstabCom]]], '<_:_|_>[{'mrx}'Principal,{'Intruder}'Intruder, '_`,_['cnt`:_[{'1}'NzMachineInt], 'dcom`:_[{'mtfield}'Field], 'roler`:_[{'mtrun}'Run], 'rolei`:_[{'mtrun}'Run], 'seckey`:_[{'skmrx}'PKey], 'ecom`:_[{'mtecom}'EstabCom], 'agents`:_['fset+[{'alice}'Principal, {'bob}'Principal, {'mrx}'Principal]], 'msgs`:_['fset+[{'mtfset}'FieldSet, 'ped[{'pkalice}'PKey, 'cat['n[{'alice}'Principal,{'1}'NzMachineInt], 'n[{'bob}'Principal,{'1}'NzMachineInt]]]]], 'ncs`:_['fset+[{'mtfset}'FieldSet, 'n[{'alice}'Principal,{'1}'NzMachineInt]]]]], 'msg[{'alice}'Principal, {'mrx}'Principal, 'ped[{'pkmrx}'PKey,'n[{'bob}'Principal,{'1}'NzMachineInt]]]]])), step( 'IntruderAcceptEveryMessage3, 0, 'boundary['__[ '<_:_|_>[{'alice}'Principal,{'NSPKAgent}'NSPKAgent, '_`,_['cnt`:_[{'2}'NzMachineInt], 'dcom`:_[{'mtfset}'FieldSet], 'roler`:_[{'mtrun}'Run], 'rolei`:_[{'mtrun}'Run], 'seckey`:_[{'skalice}'PKey], 'ecom`:_['ecom[{'i}'role, 'n[{'alice}'Principal,{'1}'NzMachineInt], {'mrx}'Principal, 'n[{'bob}'Principal,{'1}'NzMachineInt]]]]], '<_:_|_>[{'bob}'Principal,{'NSPKAgent}'NSPKAgent, '_`,_['cnt`:_[{'2}'NzMachineInt], 'dcom`:_[{'mtfield}'Field], 'roler`:_['run+[{'mtrun}'Run, 'run['n[{'bob}'Principal,{'1}'NzMachineInt], {'alice}'Principal, 'n[{'alice}'Principal,{'1}'NzMachineInt]]]], 'rolei`:_[{'mtrun}'Run], 'seckey`:_[{'skbob}'PKey], 'ecom`:_[{'mtecom}'EstabCom]]], '<_:_|_>[{'mrx}'Principal,{'Intruder}'Intruder, '_`,_['cnt`:_[{'1}'NzMachineInt], 'dcom`:_[{'mtfield}'Field], 'roler`:_[{'mtrun}'Run], 'rolei`:_[{'mtrun}'Run], 'seckey`:_[{'skmrx}'PKey], 'ecom`:_[{'mtecom}'EstabCom], 'agents`:_['fset+[{'alice}'Principal, {'bob}'Principal, {'mrx}'Principal]], 'msgs`:_['fset+[{'mtfset}'FieldSet, 'ped[{'pkalice}'PKey, 'cat['n[{'alice}'Principal,{'1}'NzMachineInt], 'n[{'bob}'Principal,{'1}'NzMachineInt]]]]], 'ncs`:_['fset+[{'mtfset}'FieldSet, 'n[{'alice}'Principal,{'1}'NzMachineInt], 'n[{'bob}'Principal,{'1}'NzMachineInt]]]]]]])), step( 'IntruderFakeMessage3, 1, 'boundary['__[ '<_:_|_>[{'alice}'Principal,{'NSPKAgent}'NSPKAgent, '_`,_['cnt`:_[{'2}'NzMachineInt], 'dcom`:_[{'mtfset}'FieldSet], 'roler`:_[{'mtrun}'Run], 'rolei`:_[{'mtrun}'Run], 'seckey`:_[{'skalice}'PKey], 'ecom`:_['ecom[{'i}'role, 'n[{'alice}'Principal,{'1}'NzMachineInt], {'mrx}'Principal, 'n[{'bob}'Principal,{'1}'NzMachineInt]]]]], '<_:_|_>[{'bob}'Principal,{'NSPKAgent}'NSPKAgent, '_`,_['cnt`:_[{'2}'NzMachineInt], 'dcom`:_[{'mtfield}'Field], 'roler`:_['run+[{'mtrun}'Run, 'run['n[{'bob}'Principal,{ '1}'NzMachineInt],{'alice}'Principal,'n[{'alice}'Principal,{'1}'NzMachineInt]]]], 'rolei`:_[{'mtrun}'Run], 'seckey`:_[{'skbob}'PKey], 'ecom`:_[{'mtecom}'EstabCom]]], '<_:_|_>[{'mrx}'Principal,{'Intruder}'Intruder, '_`,_['cnt`:_[{'1}'NzMachineInt], 'dcom`:_[{'mtfield}'Field], 'roler`:_[{'mtrun}'Run], 'rolei`:_[{'mtrun}'Run], 'seckey`:_[{'skmrx}'PKey], 'ecom`:_[{'mtecom}'EstabCom], 'agents`:_['fset+[{'alice}'Principal, {'bob}'Principal, {'mrx}'Principal]], 'msgs`:_['fset+[{'mtfset}'FieldSet, 'ped[{'pkalice}'PKey, 'cat['n[{'alice}'Principal,{'1}'NzMachineInt], 'n[{'bob}'Principal,{'1}'NzMachineInt]]]]], 'ncs`:_['fset+[{'mtfset}'FieldSet, 'n[{'alice}'Principal,{'1}'NzMachineInt], 'n[{'bob}'Principal,{'1}'NzMachineInt]]]]], 'msg[{'alice}'Principal, {'bob}'Principal, 'ped[{'pkbob}'PKey,'n[{'bob}'Principal,{'1}'NzMachineInt]]]]])), step( 'Message3Rec, 0, 'boundary['__[ '<_:_|_>[{'alice}'Principal,{'NSPKAgent}'NSPKAgent, '_`,_['cnt`:_[{'2}'NzMachineInt], 'dcom`:_[{'mtfset}'FieldSet], 'roler`:_[{'mtrun}'Run], 'rolei`:_[{'mtrun}'Run], 'seckey`:_[{'skalice}'PKey], 'ecom`:_['ecom[{'i}'role, 'n[{'alice}'Principal,{'1}'NzMachineInt], {'mrx}'Principal, 'n[{'bob}'Principal,{'1}'NzMachineInt]]]]], '<_:_|_>[{'bob}'Principal,{'NSPKAgent}'NSPKAgent, '_`,_['cnt`:_[{'2}'NzMachineInt], 'dcom`:_[{'mtfield}'Field], 'roler`:_[{'mtrun}'Run], 'rolei`:_[{'mtrun}'Run], 'seckey`:_[{'skbob}'PKey], 'ecom`:_['ecom[{'r}'role, 'n[{'bob}'Principal,{'1}'NzMachineInt], {'alice}'Principal, 'n[{'alice}'Principal,{'1}'NzMachineInt]]]]], '<_:_|_>[{'mrx}'Principal,{'Intruder}'Intruder, '_`,_['cnt`:_[{'1}'NzMachineInt], 'dcom`:_[{'mtfield}'Field], 'roler`:_[{'mtrun}'Run], 'rolei`:_[{'mtrun}'Run], 'seckey`:_[{'skmrx}'PKey], 'ecom`:_[{'mtecom}'EstabCom], 'agents`:_['fset+[{'alice}'Principal, {'bob}'Principal, {'mrx}'Principal]], 'msgs`:_['fset+[{'mtfset}'FieldSet, 'ped[{'pkalice}'PKey, 'cat['n[{'alice}'Principal,{'1}'NzMachineInt], 'n[{'bob}'Principal,{'1}'NzMachineInt]]]]], 'ncs`:_['fset+[{'mtfset}'FieldSet, 'n[{'alice}'Principal,{'1}'NzMachineInt], 'n[{'bob}'Principal,{'1}'NzMachineInt]]]]]]])), step( 'IntruderRecognizeAttack, 0, 'boundary['__[ '<_:_|_>[{'alice}'Principal,{'NSPKAgent}'NSPKAgent, '_`,_['cnt`:_[{'2}'NzMachineInt], 'dcom`:_[{'mtfset}'FieldSet], 'roler`:_[{'mtrun}'Run], 'rolei`:_[{'mtrun}'Run], 'seckey`:_[{'skalice}'PKey], 'ecom`:_['ecom[{'i}'role, 'n[{'alice}'Principal,{'1}'NzMachineInt], {'mrx}'Principal, 'n[{'bob}'Principal,{'1}'NzMachineInt]]]]], '<_:_|_>[{'bob}'Principal,{'NSPKAgent}'NSPKAgent, '_`,_['cnt`:_[{'2}'NzMachineInt], 'dcom`:_[{'mtfield}'Field], 'roler`:_[{'mtrun}'Run], 'rolei`:_[{'mtrun}'Run], 'seckey`:_[{'skbob}'PKey], 'ecom`:_['ecom[{'r}'role, 'n[{'bob}'Principal,{'1}'NzMachineInt], {'alice}'Principal, 'n[{'alice}'Principal,{'1}'NzMachineInt]]]]], '<_:_|_>[{'mrx}'Principal,{'Intruder}'Intruder, '_`,_['cnt`:_[{'1}'NzMachineInt], 'dcom`:_[{'mtfield}'Field], 'roler`:_[{'mtrun}'Run], 'rolei`:_[{'mtrun}'Run], 'seckey`:_[{'skmrx}'PKey], 'ecom`:_['ecom[{'i}'role, 'n[{'alice}'Principal,{'1}'NzMachineInt], {'bob}'Principal, 'n[{'bob}'Principal,{'1}'NzMachineInt]]], 'agents`:_['fset+[{'alice}'Principal, {'bob}'Principal, {'mrx}'Principal]], 'msgs`:_['fset+[{'mtfset }'FieldSet, 'ped[{'pkalice}'PKey, 'cat['n[{'alice}'Principal,{'1}'NzMachineInt], 'n[{'bob}'Principal,{'1}'NzMachineInt] ]]]], 'ncs`:_['fset+[{'mtfset}'FieldSet, 'n[{'alice}'Principal,{'1}'NzMachineInt], 'n[{'bob}'Principal,{'1}'NzMachineInt]]]]]]])))