loop init . (omod NSPK is protecting MACHINE-INT . protecting META-LEVEL . sort Field . sort Principal . sort Nonce . sort PKey . sort Run . sort Table . sort FieldSet . sort Role . sort EstabCom . subsorts Nonce Principal PKey Bool < Field . subsort Field < FieldSet . subsort Principal < Oid . class NSPKAgent | ecom : EstabCom, seckey : PKey, rolei : Run, roler : Run, dcom : FieldSet, cnt : MachineInt . class Intruder | ecom : EstabCom, seckey : PKey, rolei : Run, roler : Run, dcom : FieldSet, cnt : MachineInt, ncs : FieldSet, msgs : FieldSet, agents : FieldSet . msg msg : Principal Principal Field -> Msg . op boundary : Configuration -> Configuration . op attack : -> Configuration . op mtfield : -> Field . op n : Principal MachineInt -> Nonce . op cat : Nonce Nonce -> Field . op first : Field -> Nonce . op rest : Field -> Nonce . op tuple : Field Principal -> Field . op ped : PKey Field -> Field . op keypair : PKey PKey -> Bool [comm] . op mtrun : -> Run . op run : Nonce Principal Field -> Run . op run+ : Run Run -> Run [assoc comm] . op in : Field Run -> Bool . op inRuns : Run Run -> Bool . op inEstabCom : EstabCom EstabCom -> Bool . op @ : Table Principal -> PKey . op mtfset : -> FieldSet . op fset+ : FieldSet FieldSet -> FieldSet [assoc comm] . op i : -> Role . op r : -> Role . op mtecom : -> EstabCom . op ecom : Role Nonce Principal Nonce -> EstabCom . op ecom+ : EstabCom EstabCom -> EstabCom [assoc comm id: mtecom] . op pktab : -> Table . op alice : -> Principal . op bob : -> Principal . op mrx : -> Principal . op pkalice : -> PKey . op pkbob : -> PKey . op pkmrx : -> PKey . op skalice : -> PKey . op skbob : -> PKey . op skmrx : -> PKey . op cf2Obj1Comm : -> Configuration . op cf2Obj2Comm : -> Configuration . op cf2Agents1Intruder : -> Configuration . var Conf : Configuration . vars PK SK KEY : PKey . vars MES F F1 F2 : Field . vars N N1 N2 NI NR : Nonce . vars PR1 A INIT RESP RESP2 B INTR : Principal . vars FSET1 FSET2 FSET3 : FieldSet . vars EC EC2 : EstabCom . vars RI RR RUN : Run . vars ROLE ROLE2 : Role . vars ATTS ATTS2 : AttributeSet . vars INT INT2 : MachineInt . ceq ped(SK,ped(PK,MES)) = MES if keypair(PK,SK) == true . eq first(cat(N1,N2)) = N1 . eq rest(cat(N1,N2)) = N2 . eq in(F,mtrun) = false . eq in(F1, run(N1,PR1,F2)) = if (F1 == N1) or (F1 == F2) then true else false fi . eq in(F1, run+(RUN, run(N1,PR1,F2))) = if (F1 == N1) or (F1 == F2) then true else in(F1, RUN) fi . eq inRuns(RUN, mtrun) = false . eq inRuns(run(N1,A,N2), run(NI,B,NR)) = if (N1 == NI) and (A == B) and (N2 == NR) then true else false fi . eq inRuns(run(N1,A,N2), run+(RUN,run(NI,B,NR))) = if (N1 == NI) and (A == B) and (N2 == NR) then true else inRuns(run(N1,A,N2), RUN) fi . eq inEstabCom(ecom(ROLE,N1,A,N2), mtecom) = false . eq inEstabCom(ecom(ROLE,N1,A,N2), ecom+(EC,ecom(ROLE2,NR,B,NI))) = if (ROLE == ROLE2) and (A == B) and (N2 == NR) and (N1 == NI) then true else inEstabCom(ecom(ROLE,N1,A,N2), EC) fi . eq fset+(F1,F1) = F1 . eq fset+(fset+(FSET1, F1), F1) = FSET1 . eq run+(RUN,RUN) = RUN . eq keypair(pkalice,skalice) = true . eq keypair(pkbob, skbob) = true . eq keypair(pkmrx, skmrx) = true . eq keypair(pkalice, skbob) = false . eq keypair(pkalice, skmrx) = false . eq keypair(pkbob, skalice) = false . eq keypair(pkbob, skmrx) = false . eq keypair(pkmrx, skalice) = false . eq keypair(pkmrx, skbob) = false . eq @(pktab,alice) = pkalice . eq @(pktab,bob) = pkbob . eq @(pktab,mrx) = pkmrx . eq cf2Agents1Intruder = boundary( < alice : NSPKAgent | ecom : mtecom , seckey : skalice, rolei : mtrun, roler : mtrun, dcom : fset+(mtfset, mrx), cnt : 1 > < bob : NSPKAgent | ecom : mtecom , seckey : skbob, rolei : mtrun, roler : mtrun, dcom : mtfield, cnt : 1 > < mrx : Intruder | ecom : mtecom , seckey : skmrx, rolei : mtrun, roler : mtrun, dcom : mtfield, cnt : 1, ncs : mtfset, msgs : mtfset, agents : fset+(mrx, bob) >) . *** If an agent 'B receives message msg['A, 'B, 'ped['KEY, 'F]] he *** has to decide whether it is a Message1, Message2 or Message3. *** let role_i = (NI, RESP, NR) role_r = (NR, INIT, NI) *** *** if first[F] == NI in role_i *** then if A == RESP *** then IntruderMessage2RecCorrect *** else IntruderMessage2RecIncorrect (stop corresponding run) *** fi *** else if F == NR in role_r *** then if A == INIT *** then IntruderMessage3RecCorrect *** else IntruderMessage3RecIncorrect (stop corresponding run) *** fi *** else (F not in role_r neither role_i) *** IntruderMessage1Rec (new run) rl [BeginRun] : boundary( < A : NSPKAgent | rolei : RI, dcom : fset+(B,FSET1), cnt : INT > Conf) => boundary( < A : NSPKAgent | rolei : run+(RI, run(n(A,INT), B, mtfield)) , dcom : FSET1, cnt : (INT + 1) > msg(A,B,ped(@(pktab,B),tuple(n(A,INT),A))) Conf) . rl [Message1Rec] : boundary( < B : NSPKAgent | seckey : SK, rolei : RI, roler : RR, cnt : INT > msg(A, B, ped(KEY, tuple(N,INIT))) Conf) => if (keypair(SK,KEY) and (INIT == A) and not(in(N,RR)) and not(in(N,RI))) then boundary( < B : NSPKAgent | roler : run+(RR, run(n(B, INT), A, N)), cnt : (INT + 1) > msg(B,A,ped(@(pktab,A),cat(N,n(B,INT)))) Conf) else boundary( < B : NSPKAgent | roler : RR > Conf) fi . rl [Message2Rec] : boundary( < A : NSPKAgent | seckey : SK, rolei : run+(RI, run(NI, RESP, mtfield)), ecom : EC > msg(B, A, ped(KEY, cat(N1,NR))) Conf) => if keypair(KEY,SK) and (B == RESP) and (NI == N1) then boundary( < A : NSPKAgent | ecom : ecom+(EC, ecom(i,NI,B,NR)), rolei : RI > msg(A, B, ped(@(pktab,B),NR)) Conf) else boundary( < A : NSPKAgent | seckey : SK > Conf) fi . rl [Message3Rec] : boundary( < B : NSPKAgent | seckey : SK, roler : run+(RR, run(NR, INIT, NI)), ecom : EC > msg(A, B, ped(KEY, N1)) Conf) => if keypair(SK,KEY) and (NR == N1) and (INIT == A) then boundary( < B : NSPKAgent | roler : RR, ecom : ecom+(EC, ecom(r,NR,A,NI)) > Conf) else boundary( < B : NSPKAgent | seckey : SK > Conf) fi . *** *** Definition of Intruder Rules *** *** Intruder behaves as if he was a normal agent but additionally *** stores all the information he gets (such as nonces, addresses of *** agents, etc) to be able to exploit them in possible attack. rl [IntruderBeginRun]: boundary( < INTR : Intruder | ncs : FSET1, agents : FSET2, rolei : RI, dcom : fset+(A, FSET3), cnt : INT > Conf) => boundary( < INTR : Intruder | ncs : fset+(n(INTR,INT), FSET1), agents : fset+(FSET2, A), rolei : run+(RI, run(n(INTR,INT), A, mtfield)), dcom : FSET3, cnt : (INT + 1) > msg(INTR, A,ped(@(pktab,A),n(INTR,INT))) Conf) . crl [IntruderMessage1Rec]: boundary( < INTR : Intruder | ncs : FSET1, agents : FSET2, rolei : RI, seckey : SK, roler : RR, cnt : INT > msg(A, INTR, ped(KEY, F)) Conf) => boundary( < INTR : Intruder | ncs : fset+(fset+(FSET1, F), n(INTR, INT)), roler : run+(RR, run(n(INTR, INT), A, F)), agents : fset+(FSET2, A), cnt : (INT + 1) > msg(INTR, A, ped(@(pktab,A), cat(F, n(INTR,INT)))) Conf) if (keypair(KEY, SK) and not(in(F, RR)) and not(in(first(F), RI)) == true ) . crl [IntruderMessage2RecCorrect]: boundary( < INTR : Intruder | ecom : EC, ncs : FSET1, seckey : SK, rolei : run+(RI, run(NI, RESP, mtfield)) > msg(A, INTR, ped(KEY, F)) Conf) => boundary( < INTR : Intruder | ecom : ecom+(EC, ecom(i,NI,A,rest(F))), ncs : fset+(FSET1, rest(F)), rolei : RI > msg(INTR, A, ped(@(pktab,A),rest(F))) Conf) if (keypair(KEY, SK) and (NI == first(F)) and (A == RESP) == true) . crl [IntruderMessage2RecIncorrect]: boundary( < INTR : Intruder | ncs : FSET1, agents : FSET2, seckey : SK, rolei : run+(RI, run(NI, RESP, mtfield)) > msg(A, INTR, ped(KEY, F)) Conf) => boundary( < INTR : Intruder | ncs : fset+(FSET1, rest(F)), agents : fset+(FSET2, A), rolei : RI > Conf) if (keypair(KEY, SK) and (NI == first(F)) and (A =/= RESP) == true) . crl [IntruderMessage3RecCorrect]: boundary( < INTR : Intruder | ecom : EC, seckey : SK, roler : run+(RR, run(NR, INIT, NI)) > msg(A, INTR, ped(KEY, F)) Conf) => boundary( < INTR : Intruder | ecom : ecom+(EC, ecom(r,NR,A,NI)), roler : RR > Conf) if (keypair(KEY, SK) and (NR == F) and (INIT == A)) == true . crl [IntruderMessage3RecIncorrect]: boundary( < INTR : Intruder | agents : FSET1, seckey : SK, roler : run+(RR, run(NR, INIT, NI)) > msg(A, INTR, ped(KEY, F)) Conf) => boundary( < INTR : Intruder | agents : fset+(FSET1, A), roler : RR > Conf) if (keypair(KEY, SK) and (NR == F) and (INIT =/= A)) == true . *** reasons for condition in intercept/overhear rule: *** 1. Intruder should not intercept/overhear those messages it sent out *** itself *as* an Intruder (because this is no new information for *** the intruder and moreover, the intruder has some intention by *** sending them out, thus, they should arrive at their destination) *** 2. Intruder need not intercept those message which are sent to him *** This rule still allows that the Intruder is intercepting messages *** which are sent by himself in the name of another agent (the *** problem is that we can not derive from looking at the message who *** actually sent it) *** See also the rule "IntruderAcceptsEveryMessage" which reflects the *** case where ==(A, INTR) crl [IntruderInterceptMessage1]: boundary( < INTR : Intruder | ncs : FSET1, msgs : FSET2, agents : FSET3, seckey : SK > msg(B, A, ped(KEY, tuple(N,A))) Conf) => if keypair(KEY, SK) then boundary( < INTR : Intruder | ncs : fset+(FSET1, N), agents : fset+(fset+(FSET3, A), B) > Conf) else boundary( < INTR : Intruder | msgs : fset+(FSET2, ped(KEY,tuple(N,A))), agents : fset+(fset+(FSET3, A), B) > Conf) fi if ((A =/= INTR) and (B =/= INTR)) == true . crl [IntruderInterceptMessage2]: boundary( < INTR : Intruder | ncs : FSET1, msgs : FSET2, agents : FSET3, seckey : SK > msg(B, A, ped(KEY, cat(N1,N2))) Conf) => if keypair(KEY, SK) then boundary( < INTR : Intruder | ncs : fset+(fset+(FSET1, N1),N2), agents : fset+(fset+(FSET3, A), B) > Conf) else boundary( < INTR : Intruder | msgs : fset+(FSET2, ped(KEY, cat(N1,N2))), agents : fset+(fset+(FSET3, A), B) > Conf) fi if ((A =/= INTR) and (B =/= INTR)) == true . crl [IntruderInterceptMessage3]: boundary( < INTR : Intruder | ncs : FSET1, msgs : FSET2, agents : FSET3, seckey : SK > msg(B, A, ped(KEY, N)) Conf) => if keypair(KEY, SK) then boundary( < INTR : Intruder | ncs : fset+(FSET1, N), agents : fset+(fset+(FSET3, A), B) > Conf) else boundary( < INTR : Intruder | msgs : fset+(FSET2, ped(KEY, N)), agents : fset+(fset+(FSET3, A), B) > Conf) fi if ((A =/= INTR) and (B =/= INTR)) == true . crl [IntruderOverhearMessage1]: boundary( < INTR : Intruder | ncs : FSET1, msgs : FSET2, agents : FSET3, seckey : SK > msg(B, A, ped(KEY, tuple(N,A))) Conf) => if keypair(KEY, SK) then boundary( < INTR : Intruder | ncs : fset+(FSET1, N), agents : fset+(fset+(FSET3, A), B) > msg(B, A, ped(KEY, F)) Conf) else boundary( < INTR : Intruder | msgs : fset+(FSET2, ped(KEY,tuple(N,A))), agents : fset+(fset+(FSET3, A), B) > msg(B, A, ped(KEY, tuple(N,A))) Conf) fi if ((A =/= INTR) and (B =/= INTR)) == true . crl [IntruderOverhearMessage2]: boundary( < INTR : Intruder | ncs : FSET1, msgs : FSET2, agents : FSET3, seckey : SK > msg(B, A, ped(KEY,cat(N1,N2))) Conf) => if keypair(KEY, SK) then boundary( < INTR : Intruder | ncs : fset+(fset+(FSET1, N1),N2), agents : fset+(fset+(FSET3, A), B) > msg(B, A, ped(KEY, F)) Conf) else boundary( < INTR : Intruder | msgs : fset+(FSET2, ped(KEY, cat(N1,N2))), agents : fset+(fset+(FSET3, A), B) > msg(B, A, ped(KEY,cat(N1,N2))) Conf) fi if ((A =/= INTR) and (B =/= INTR)) == true . crl [IntruderOverhearMessage3]: boundary( < INTR : Intruder | ncs : FSET1, msgs : FSET2, agents : FSET3, seckey : SK > msg(B, A, ped(KEY, N)) Conf) => if keypair(KEY, SK) then boundary( < INTR : Intruder | ncs : fset+(FSET1, N), agents : fset+(fset+(FSET3, A), B) > msg(B, A, ped(KEY, N)) Conf) else boundary( < INTR : Intruder | msgs : fset+(FSET2, ped(KEY, N)), agents : fset+(fset+(FSET3, A), B) > msg(B, A, ped(KEY, N)) Conf) fi if ((A =/= INTR) and (B =/= INTR)) == true . *** conditional rule to make sure that no empty messages are sent and *** the intruder does not replay message for himself crl [IntruderReplayMessage] : boundary( < INTR : Intruder | msgs : fset+(FSET1, MES), agents : fset+(fset+(FSET2, A), B) > Conf) => boundary( < INTR : Intruder | msgs : fset+(FSET1, MES), agents : fset+(fset+(FSET2, A), B) > msg(B, A, MES) Conf) if ((MES =/= mtfield) and (A =/= INTR)) == true . *** Fake messages from known nonces, etc *** condition to make sure the intruder never fakes a message to himself crl [IntruderFakeMessage1] : boundary( < INTR : Intruder | ncs : fset+(FSET1, N), agents : fset+(fset+(FSET2, B), A) > Conf) => boundary( < INTR : Intruder | ncs : fset+(FSET1, N) > msg(A, B, ped(@(pktab,B), tuple(N,A))) Conf) if (B =/= INTR) == true . crl [IntruderFakeMessage2] : boundary( < INTR : Intruder | ncs : fset+(FSET1, N), agents : fset+(fset+(FSET2, B), A) > Conf) => boundary( < INTR : Intruder | ncs : fset+(fset+(FSET1, N1), N2) > msg(A, B, ped(@(pktab,B), cat(N1,N2))) Conf) if (B =/= INTR) == true . crl [IntruderFakeMessage3] : boundary( < INTR : Intruder | ncs : fset+(FSET1, N), agents : fset+(fset+(FSET2, B), A) > Conf) => boundary( < INTR : Intruder | ncs : fset+(FSET1, N) > msg(A, B, ped(@(pktab,B), N)) Conf) if (B =/= INTR) == true . *** Whatever is sent to the Intruder, the intruder will accept it, *** whether or not it fits his runs (since the intruder is always *** eager to learn new things) *** (e.g. used in the attack, penultimate step) *** 3 different rules, one for each "kind" of message crl [IntruderAcceptEveryMessage1]: boundary( < INTR : Intruder | ncs : FSET1, msgs : FSET2, agents : FSET3, seckey : SK > msg(A, INTR, ped(KEY, tuple(N,A))) Conf) => if keypair(KEY, SK) then boundary( < INTR : Intruder | ncs : fset+(FSET1, N), agents : fset+(FSET3, A) > Conf) else boundary( < INTR : Intruder | msgs : fset+(FSET2, ped(KEY,tuple(N,A))), agents : fset+(FSET3, A) > Conf) fi if (A =/= INTR) == true . crl [IntruderAcceptEveryMessage2]: boundary( < INTR : Intruder | ncs : FSET1, msgs : FSET2, agents : FSET3, seckey : SK > msg(A, INTR, ped(KEY, cat(N1,N2))) Conf) => if keypair(KEY, SK) then boundary( < INTR : Intruder | ncs : fset+(fset+(FSET1, N1),N2), agents : fset+(FSET3, A) > Conf) else boundary( < INTR : Intruder | msgs : fset+(FSET2, ped(KEY,cat(N1,N2))), agents : fset+(FSET3, A) > Conf) fi if (A =/= INTR) == true . crl [IntruderAcceptEveryMessage3]: boundary( < INTR : Intruder | ncs : FSET1, msgs : FSET2, agents : FSET3, seckey : SK > msg(A, INTR, ped(KEY, N)) Conf) => if keypair(KEY, SK) then boundary( < INTR : Intruder | ncs : fset+(FSET1, N), agents : fset+(FSET3, A) > Conf) else boundary( < INTR : Intruder | msgs : fset+(FSET2, ped(KEY,N)), agents : fset+(FSET3, A) > Conf) fi if (A =/= INTR) == true . *** If an agent established a communication with another agent and the *** intruder knows all used nonces, an attack was *** successful. Therefore, the intruder recognizes the attack and *** stores the information as an established communication with him. *** The condition assures that only REAL attacks are recognized, i.e., *** if the intruder acts as a normal agent and has established or is *** about to establish (nonces in runs) a communication with another *** agent, then this is no attack crl [IntruderRecognizeAttack] : boundary( < INTR : Intruder | ecom : EC, rolei : RI, roler : RR, ncs : fset+(fset+(FSET1, N1), N2) > < A : NSPKAgent | ecom : ecom+(EC2, ecom(ROLE,N1,B,N2)) > Conf) => if (ROLE == i) then boundary( < INTR : Intruder | ecom : ecom+(EC, ecom(r,N2,A,N1)) > < A : NSPKAgent | ecom : ecom+(EC2, ecom(ROLE,N1,B,N2)) > Conf) else boundary( < INTR : Intruder | ecom : ecom+(EC, ecom(i,N2,A,N1)) > < A : NSPKAgent | ecom : ecom+(EC2, ecom(ROLE,N1,B,N2)) > Conf) fi if (not(inEstabCom(ecom(r,N2,A,N1),EC)) and not(inEstabCom(ecom(i,N2,A,N1), EC)) and not(in(N1,RI)) and not(in(N1,RR)) and not(in(N2,RI)) and not(in(N2,RR)) and B =/= INTR) == true . rl [Initial2Obj1Comm] : cf2Obj1Comm => boundary( < alice : NSPKAgent | ecom : mtecom , seckey : skalice, rolei : mtrun, roler : mtrun, dcom : fset+(mtfset, bob), cnt : 1 > < bob : NSPKAgent | ecom : mtecom , seckey : skbob, rolei : mtrun, roler : mtrun, dcom : mtfield, cnt : 1 >) . rl [Initial2Obj2Comm] : cf2Obj2Comm => boundary( < alice : NSPKAgent | ecom : mtecom , seckey : skalice, rolei : mtrun, roler : mtrun, dcom : fset+(mtfset, bob), cnt : 1 > < bob : NSPKAgent | ecom : mtecom , seckey : skbob, rolei : mtrun, roler : mtrun, dcom : fset+(mtfset, alice), cnt : 1 >) . endom) (fmod SEARCH is protecting META-LEVEL[NSPK] . ******************** SEARCH STRATEGY ******************************* ******************************************************************** sorts Strategy Path Step . subsort Term < Path . var Labels : QidList . var StopLabels : QidSet . var APath : Path . vars QIList QIList' : QidList . var T : Term . var L QI QI' : Qid . var N : MachineInt . var SS : QidSet . var M : Module . var MaxDepth Depth : MachineInt . var SB : Substitution . op extTerm : ResultPair -> Term . op extSubst : ResultPair -> Substitution . eq extSubst({T, SB}) = SB . eq extTerm({T, SB}) = T . op step : Qid MachineInt Term -> Step . op noStep : -> Step . op path : Path Step -> Path . op emptyPath : -> Path . op lastTerm : Path -> Term . op rest : Qid QidList -> QidList . op memberQidQidSet : Qid QidSet -> Bool . eq rest(QI, (((QIList QI) QI') QIList')) = (QI' QIList') . eq rest(QI, (QIList QI)) = nil . eq lastTerm(path(APath, step(L, N, T))) = T . eq lastTerm(T) = T . eq memberQidQidSet(QI, (QI ; SS) ) = true . op stop : MachineInt Path -> Strategy . op boundedDepthFirstSearchUntilStopRules : Module Term QidList QidSet MachineInt -> Strategy . op boundedDepthFirstSearchUntilStopRulesAux : Module MachineInt Path QidList QidSet MachineInt -> Strategy . op backtrack : Module MachineInt Path QidList QidSet MachineInt -> Strategy . op nextRewrite : Module Term QidList -> Step . eq boundedDepthFirstSearchUntilStopRules(M, T, Labels, StopLabels, MaxDepth) = boundedDepthFirstSearchUntilStopRulesAux(M, 0, T, Labels, StopLabels, MaxDepth) . eq boundedDepthFirstSearchUntilStopRulesAux( M, 0, T, Labels, StopLabels, MaxDepth) = if nextRewrite(M, T, Labels) == noStep then stop(0, emptyPath) else boundedDepthFirstSearchUntilStopRulesAux( M, 1, path(T, nextRewrite(M, T, Labels)), Labels, StopLabels, MaxDepth) fi . eq boundedDepthFirstSearchUntilStopRulesAux( M, Depth, path(APath, step(L, N, T)), Labels, StopLabels, MaxDepth) = if memberQidQidSet(L, StopLabels) == true then stop(Depth, path(APath, step(L, N, T))) else (if Depth < MaxDepth then (if nextRewrite(M, T, Labels) == noStep then backtrack(M, Depth, path(APath, step(L, N, T)), Labels, StopLabels, MaxDepth) else boundedDepthFirstSearchUntilStopRulesAux( M, Depth + 1, path(path(APath, step(L, N, T)), nextRewrite(M, T, Labels)), Labels, StopLabels, MaxDepth) fi) else backtrack(M, Depth, path(APath, step(L, N, T)), Labels, StopLabels, MaxDepth) fi) fi . eq backtrack( M, Depth, path(APath, step(L, N, T)), Labels, StopLabels, MaxDepth) = if (meta-apply(M, lastTerm(APath), L, none, N + 1) == {error*, none}) then (if (nextRewrite(M, lastTerm(APath), rest(L, Labels)) == noStep) then backtrack(M, _-_(Depth , 1), APath, Labels, StopLabels, MaxDepth) else boundedDepthFirstSearchUntilStopRulesAux( M, Depth, path(APath, nextRewrite(M, lastTerm(APath), rest(L, Labels))), Labels, StopLabels, MaxDepth) fi) else boundedDepthFirstSearchUntilStopRulesAux( M, Depth, path(APath, step(L, N + 1, extTerm(meta-apply(M, lastTerm(APath), L, none, N + 1)))), Labels, StopLabels, MaxDepth) fi . eq backtrack(M, 0, T, Labels, StopLabels, MaxDepth) = stop(0, emptyPath) . eq nextRewrite(M, T, nil) = noStep . eq nextRewrite(M, T,(L Labels)) = if (meta-apply(M, T, L, none, 0) == {error*, none}) then nextRewrite(M, T, Labels) else step(L, 0, extTerm(meta-apply(M, T, L, none, 0))) fi . var StartDepth : MachineInt . op breadthFirstSearchUntilStopRules : Module Term QidList QidSet MachineInt -> Strategy . eq breadthFirstSearchUntilStopRules(M, T, Labels, StopLabels, StartDepth) = if boundedDepthFirstSearchUntilStopRules( M, T, Labels, StopLabels, StartDepth) == stop(0, emptyPath) then boundedDepthFirstSearchUntilStopRules( M, T, Labels, StopLabels, StartDepth + 1) else boundedDepthFirstSearchUntilStopRules( M, T, Labels, StopLabels, StartDepth) fi . endfm)