load test0-lookup.m
load model-checker
load ../ALL/simple.m
load ../ALL/mc.m

mod MC0 is
  inc MC .
  inc TEST0-LOOKUP .

endm

***(

red findPath(st(icf, prop0 ) .
red findPath(st(icf, prop1 ) .
red findPath(st(icf, prop2 ) .
red findPath(st(icf, prop3 ) .

 red findPath(st(icf),prop0) .
reduce in MC0 : findPath(st(icf), prop0) .
rewrites: 1024 in 110ms cpu (132ms real) (9309 rewrites/second)
result SimplePath: spath('ssptk.regreq 'jvm.dispatch 'xmit 'jvm.deliver
    'lookup.register 'jvm.dispatch 'xmit 'jvm.deliver 'ssptk.regreply
    'ssptk.regreq 'jvm.dispatch 'xmit 'jvm.deliver 'lookup.register
    'jvm.dispatch 'xmit 'jvm.deliver 'ssptk.regreply 'app.findsvc
    'csptk.findServiceReq 'jvm.dispatch 'xmit 'jvm.deliver 'lookup.lookup
    'jvm.dispatch 'xmit 'jvm.deliver 'csptk.lookupOk 'jvm.new 'csptk.newidreply
    'app.foundsvc 'cssp.svcreq 'jvm.dispatch 'xmit 'jvm.deliver 'svc.svcreq
    'jvm.dispatch 'xmit 'jvm.deliver 'cssp.svcreply 'app.svcans 'app.findsvc
    'cssp.svcreq 'jvm.dispatch 'xmit 'jvm.deliver 'svc.svcreq 'jvm.dispatch
    'xmit 'jvm.deliver 'cssp.svcreply 'app.svcans, st(
< eee : Transmitter | inQ(none),outQ(none) > 
< JL : JVM | oCtr(0),
 {
< JL . AttackSvc : SVC | state(update(update(attackData, mycall, "sam"),
    badcall, "sam")) > 
< JL . csptk : CSPTK0 | idle,clientId(fakeId),lookup(JL . lup) > 
< JL . app : AttackerApp | idle,myCall(acall),myTK(JL . csptk) > 
< JL . lup : AttackerLookup | svcSet(proxyD(CP0, svc(JS . GBPsvc)) proxyD(CP0,
    svc(JS . USsvc))),attackeeSet(proxyD(CP0, svc(JS . GBPsvc)) proxyD(CP0,
    svc(JS . USsvc))),myCPTK(JL . csptk),myPxd(proxyD(CP0, svc(JL .
    AttackSvc))),svctable(("GBPquote" := proxyD(CP0, svc(JS . GBPsvc))),
    "USquote" := proxyD(CP0, svc(JS . USsvc))) >},ether(eee) > 
< JS : JVM | oCtr(0),
 {
< JS . GBPsvc : SVC | state(GBPdata) > 
< JS . USsvc : SVC | state(USdata) > 
< JS . ssptk : SSPTK0 | idle,lookup(JL . lup) > 
msg(JS . fred, JS . ssptk, registerReply) 
msg(JS . fred, JS . ssptk, registerReply)},ether(eee) > 
< JC : JVM | oCtr(1),
 {
< JC . csptk : CSPTK0 | idle,clientId("sam"),lookup(JL . lup) > 
< JC . app : APP | idle,svcFound(b("GBPquote", JC . o(0))),mytk(JC . csptk) > 
< JC . o(0) : CP0 | idle,svc(JL . AttackSvc),clientId("sam") > 
msg(JC . sam, JC . app, svcAns("GBPquote", reply(attackData, mycall, "sam"))) 
msg(JC . sam, JC . app, svcAns("GBPquote", reply(update(attackData, mycall,
    "sam"), badcall, "sam")))},ether(eee) >))

Maude> red findPath(st(icf),prop1) .
reduce in MC0 : findPath(st(icf), prop1) .
rewrites: 936 in 60ms cpu (63ms real) (15600 rewrites/second)
result SimplePath: spath('ssptk.regreq 'jvm.dispatch 'xmit 'jvm.deliver
    'lookup.register 'jvm.dispatch 'xmit 'jvm.deliver 'ssptk.regreply
    'ssptk.regreq 'jvm.dispatch 'xmit 'jvm.deliver 'lookup.register
    'jvm.dispatch 'xmit 'jvm.deliver 'ssptk.regreply 'app.findsvc
    'csptk.findServiceReq 'jvm.dispatch 'xmit 'jvm.deliver 'lookup.lookup
    'jvm.dispatch 'xmit 'jvm.deliver 'csptk.lookupOk 'jvm.new
    'csptk.newidreply, st(
< eee : Transmitter | inQ(none),outQ(none) > 
< JL : JVM | oCtr(0),
 {
< JL . AttackSvc : SVC | state(attackData) > 
< JL . csptk : CSPTK0 | idle,clientId(fakeId),lookup(JL . lup) > 
< JL . app : AttackerApp | idle,myCall(acall),myTK(JL . csptk) > 
< JL . lup : AttackerLookup | svcSet(proxyD(CP0, svc(JS . GBPsvc)) proxyD(CP0,
    svc(JS . USsvc))),attackeeSet(proxyD(CP0, svc(JS . GBPsvc)) proxyD(CP0,
    svc(JS . USsvc))),myCPTK(JL . csptk),myPxd(proxyD(CP0, svc(JL .
    AttackSvc))),svctable(("GBPquote" := proxyD(CP0, svc(JS . GBPsvc))),
    "USquote" := proxyD(CP0, svc(JS . USsvc))) >},ether(eee) > 
< JS : JVM | oCtr(0),
 {
< JS . GBPsvc : SVC | state(GBPdata) > 
< JS . USsvc : SVC | state(USdata) > 
< JS . ssptk : SSPTK0 | idle,lookup(JL . lup) > 
msg(JS . fred, JS . ssptk, registerReply) 
msg(JS . fred, JS . ssptk, registerReply)},ether(eee) > 
< JC : JVM | oCtr(1),
 {
< JC . csptk : CSPTK0 | idle,clientId("sam"),lookup(JL . lup) > 
< JC . app : APP | svcFound(none),mytk(JC . csptk),waitfor(JC . csptk, JC .
    sam, svcCall("GBPquote", mycall)) > 
< JC . o(0) : CP0 | idle,svc(JL . AttackSvc),clientId("sam") > 
msg(JC . app, JC . csptk, findServiceOk("GBPquote", JC . o(0))) 
msg(JC . app, JC . sam, svcCall("GBPquote", badcall))},ether(eee) >))

-----------------------------------------------------------------------
red findPath(st(icf),prop2) .
reduce in MC0 : findPath(st(icf), prop2) .
rewrites: 960 in 70ms cpu (66ms real) (13714 rewrites/second)
result SimplePath: spath('ssptk.regreq 'jvm.dispatch 'xmit 'jvm.deliver
    'lookup.register 'jvm.dispatch 'xmit 'jvm.deliver 'ssptk.regreply
    'ssptk.regreq 'jvm.dispatch 'xmit 'jvm.deliver 'lookup.register
    'jvm.dispatch 'xmit 'jvm.deliver 'ssptk.regreply 'app.findsvc
    'csptk.findServiceReq 'jvm.dispatch 'xmit 'jvm.deliver 'lookup.lookup
    'jvm.dispatch 'xmit 'jvm.deliver 'csptk.lookupOk 'jvm.new
    'csptk.newidreply, st(
< eee : Transmitter | inQ(none),outQ(none) > 
< JL : JVM | oCtr(0),
 {
< JL . AttackSvc : SVC | state(attackData) > 
< JL . csptk : CSPTK0 | idle,clientId(fakeId),lookup(JL . lup) > 
< JL . app : AttackerApp | idle,myCall(acall),myTK(JL . csptk) > 
< JL . lup : AttackerLookup | svcSet(proxyD(CP0, svc(JS . GBPsvc)) proxyD(CP0,
    svc(JS . USsvc))),attackeeSet(proxyD(CP0, svc(JS . GBPsvc)) proxyD(CP0,
    svc(JS . USsvc))),myCPTK(JL . csptk),myPxd(proxyD(CP0, svc(JL .
    AttackSvc))),svctable(("GBPquote" := proxyD(CP0, svc(JS . GBPsvc))),
    "USquote" := proxyD(CP0, svc(JS . USsvc))) >},ether(eee) > 
< JS : JVM | oCtr(0),
 {
< JS . GBPsvc : SVC | state(GBPdata) > 
< JS . USsvc : SVC | state(USdata) > 
< JS . ssptk : SSPTK0 | idle,lookup(JL . lup) > 
msg(JS . fred, JS . ssptk, registerReply) 
msg(JS . fred, JS . ssptk, registerReply)},ether(eee) > 
< JC : JVM | oCtr(1),
 {
< JC . csptk : CSPTK0 | idle,clientId("sam"),lookup(JL . lup) > 
< JC . app : APP | svcFound(none),mytk(JC . csptk),waitfor(JC . csptk, JC .
    sam, svcCall("GBPquote", mycall)) > 
< JC . o(0) : CP0 | idle,svc(JL . AttackSvc),clientId("sam") > 
msg(JC . app, JC . csptk, findServiceOk("GBPquote", JC . o(0))) 
msg(JC . app, JC . sam, svcCall("GBPquote", badcall))},ether(eee) >))

red findPath(st(icf),prop3) .
reduce in MC0 : findPath(st(icf), prop3) .
rewrites: 949 in 60ms cpu (63ms real) (15816 rewrites/second)
result SimplePath: spath(nil, st(
< eee : Transmitter | inQ(none),outQ(none) > 
< JL : JVM | oCtr(0),
 {
< JL . AttackSvc : SVC | state(attackData) > 
< JL . csptk : CSPTK0 | idle,clientId(fakeId),lookup(JL . lup) > 
< JL . app : AttackerApp | idle,myCall(acall),myTK(JL . csptk) > 
< JL . lup : AttackerLookup | svcSet(none),attackeeSet(none),myCPTK(JL .
    csptk),myPxd(proxyD(CP0, svc(JL . AttackSvc))),svctable(none) >},ether(eee)
    > 
< JS : JVM | oCtr(0),
 {
< JS . GBPsvc : SVC | state(GBPdata) > 
< JS . USsvc : SVC | state(USdata) > 
< JS . ssptk : SSPTK0 | idle,lookup(JL . lup) > 
msg(JS . ssptk, JS . fred, spRegisterReq("GBPquote", JS . GBPsvc)) 
msg(JS . ssptk, JS . fred, spRegisterReq("USquote", JS . USsvc))},ether(eee) > 
< JC : JVM | oCtr(0),
 {
< JC . csptk : CSPTK0 | idle,clientId("sam"),lookup(JL . lup) > 
< JC . app : APP | idle,svcFound(none),mytk(JC . csptk) > 
msg(JC . app, JC . sam, svcCall("GBPquote", mycall)) 
msg(JC . app, JC . sam, svcCall("GBPquote", badcall))},ether(eee) >))


)