mod MC1 is
  inc SIMPLE .
  inc SPTK1-TEST .

  op st : Configuration -> State .

  op prop1 : -> Prop .
  eq  st(C:Configuration 
         < JC : JVM | jatts:AttributeSet,
           { jconf:Configuration
             msg(JC . sam, JC . app, svcAns(sn1:String, d1:Data)) 
             msg(JC . sam, JC . app, svcAns(sn2:String, d2:Data)) } > )
      sat prop1 = true .
endm

***(

findPath(st(eecf sjcf ljcf cjcf), prop1 ) .
result SimplePath: spath('ssptk.regreq 'jvm.new 'ssptk.sapId 'jvm.dispatch
    'xmit 'jvm.deliver 'lookup.register 'jvm.dispatch 'xmit 'jvm.deliver
    'ssptk.regreply 'ssptk.regreq 'jvm.new 'ssptk.sapId '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 'sssp.svcreq 'svc.svcreq 'sssp.reply
    'jvm.dispatch 'xmit 'jvm.deliver 'cssp.svcreply 'app.svcans 'app.findsvc
    'cssp.svcreq 'jvm.dispatch 'xmit 'jvm.deliver 'sssp.svcreq 'svc.svcreq
    'sssp.reply 'jvm.dispatch 'xmit 'jvm.deliver 'cssp.svcreply 'app.svcans,
    st(
< eee : Transmitter | inQ(none),outQ(none) > 
< JL : JVM | oCtr(0),
 {
< JL . lup : LOOKUP | svctable(("GBPquote" := proxyD(CSP1, svc(JS . o(0)))),
    "USquote" := proxyD(CSP1, svc(JS . o(1)))) >},ether(eee) > 
< JS : JVM | oCtr(2),
 {
< JS . GBPsvc : SVC | state(update(update(GBPdata, mycall, "sam"), badcall,
    "sam")) > 
< JS . USsvc : SVC | state(USdata) > 
< JS . ssptk : SSPTK1 | idle,lookup(JL . lup) > 
< JS . o(0) : SSP1 | idle,svc(JS . GBPsvc) > 
< JS . o(1) : SSP1 | idle,svc(JS . USsvc) > 
msg(JS . fred, JS . ssptk, registerReply) 
msg(JS . fred, JS . ssptk, registerReply)},ether(eee) > 
< JC : JVM | oCtr(1),
 {
< JC . csptk : CSPTK1 | idle,clientId("sam"),lookup(JL . lup) > 
< JC . app : APP | idle,svcFound(b("GBPquote", JC . o(0))),mytk(JC . csptk) > 
< JC . o(0) : CSP1 | idle,svc(JS . o(0)),clientId("sam") > 
msg(JC . sam, JC . app, svcAns("GBPquote", reply(GBPdata, mycall, "sam"))) 
msg(JC . sam, JC . app, svcAns("GBPquote", reply(update(GBPdata, mycall,
    "sam"), badcall, "sam")))},ether(eee) >))

======================================================================
red findPath(st(eacf sjcf ljcf cjcf), prop1) .
reduce in MC1 : findPath(st(eacf sjcf cjcf ljcf), prop1) .
rewrites: 650 in 40ms cpu (40ms real) (16250 rewrites/second)
result SimplePath: spath('ssptk.regreq 'jvm.new 'ssptk.sapId 'jvm.dispatch
    'attack.registerReq 'jvm.deliver 'ssptk.regreply 'ssptk.regreq 'jvm.new
    'ssptk.sapId 'jvm.dispatch 'attack.registerReq 'jvm.deliver 'ssptk.regreply
    'app.findsvc 'csptk.findServiceReq 'jvm.dispatch 'attack.lookupReq
    'jvm.deliver 'csptk.lookupOk 'jvm.new 'csptk.newidreply 'app.foundsvc
    'cssp.svcreq 'jvm.dispatch 'xmit.smsg 'jvm.deliver 'sssp.svcreq 'svc.svcreq
    'sssp.reply 'jvm.dispatch 'xmit.smsg 'jvm.deliver 'cssp.svcreply
    'app.svcans 'app.findsvc 'cssp.svcreq 'jvm.dispatch 'xmit.smsg 'jvm.deliver
    'sssp.svcreq 'svc.svcreq 'sssp.reply 'jvm.dispatch 'xmit.smsg 'jvm.deliver
    'cssp.svcreply 'app.svcans, st(
< eee : Attacker | inQ(none),outQ(none),clientIds(none),clientDs(none),pxDs(
    proxyD(CSP1, svc(JS . o(0))) proxyD(CSP1, svc(JS . o(1)))) > 
< JL : JVM | oCtr(0),
 {
< JL . lup : LOOKUP | svctable(none) >},ether(eee) > 
< JS : JVM | oCtr(2),
 {
< JS . GBPsvc : SVC | state(update(update(GBPdata, mycall, "sam"), badcall,
    "sam")) > 
< JS . USsvc : SVC | state(USdata) > 
< JS . ssptk : SSPTK1 | idle,lookup(JL . lup) > 
< JS . o(0) : SSP1 | idle,svc(JS . GBPsvc) > 
< JS . o(1) : SSP1 | idle,svc(JS . USsvc) > 
msg(JS . fred, JS . ssptk, registerReply) 
msg(JS . fred, JS . ssptk, registerReply)},ether(eee) > 
< JC : JVM | oCtr(1),
 {
< JC . csptk : CSPTK1 | idle,clientId("sam"),lookup(JL . lup) > 
< JC . app : APP | idle,svcFound(b("GBPquote", JC . o(0))),mytk(JC . csptk) > 
< JC . o(0) : CSP1 | idle,svc(JS . o(0)),clientId("sam") > 
msg(JC . sam, JC . app, svcAns("GBPquote", reply(GBPdata, mycall, "sam"))) 
msg(JC . sam, JC . app, svcAns("GBPquote", reply(update(GBPdata, mycall,
    "sam"), badcall, "sam")))},ether(eee) >))

======================================================================
red findPath(st(eecf sjcf ljcf cjcf ajcf), prop1) .
reduce in MC1 : findPath(st(eecf sjcf ljcf ajcf cjcf), prop1) .
rewrites: 1242 in 80ms cpu (81ms real) (15525 rewrites/second)
result SimplePath: spath('ssptk.regreq 'jvm.new 'ssptk.sapId 'jvm.dispatch
    'xmit 'jvm.deliver 'lookup.register 'jvm.dispatch 'xmit 'jvm.deliver
    'ssptk.regreply 'ssptk.regreq 'jvm.new 'ssptk.sapId '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 'sssp.svcreq 'svc.svcreq 'sssp.reply
    'jvm.dispatch 'xmit 'jvm.deliver 'cssp.svcreply 'app.svcans 'app.findsvc
    'cssp.svcreq 'jvm.dispatch 'xmit 'jvm.deliver 'sssp.svcreq 'svc.svcreq
    'sssp.reply 'jvm.dispatch 'xmit 'jvm.deliver 'cssp.svcreply 'app.svcans,
    st(
< eee : Transmitter | inQ(none),outQ(none) > 
< JL : JVM | oCtr(0),
 {
< JL . lup : LOOKUP | svctable(("GBPquote" := proxyD(CSP1, svc(JS . o(0)))),
    "USquote" := proxyD(CSP1, svc(JS . o(1)))) >},ether(eee) > 
< JS : JVM | oCtr(2),
 {
< JS . GBPsvc : SVC | state(update(update(GBPdata, mycall, "sam"), badcall,
    "sam")) > 
< JS . USsvc : SVC | state(USdata) > 
< JS . ssptk : SSPTK1 | idle,lookup(JL . lup) > 
< JS . o(0) : SSP1 | idle,svc(JS . GBPsvc) > 
< JS . o(1) : SSP1 | idle,svc(JS . USsvc) > 
msg(JS . fred, JS . ssptk, registerReply) 
msg(JS . fred, JS . ssptk, registerReply)},ether(eee) > 
< JC : JVM | oCtr(1),
 {
< JC . csptk : CSPTK1 | idle,clientId("sam"),lookup(JL . lup) > 
< JC . app : APP | idle,svcFound(b("GBPquote", JC . o(0))),mytk(JC . csptk) > 
< JC . o(0) : CSP1 | idle,svc(JS . o(0)),clientId("sam") > 
msg(JC . sam, JC . app, svcAns("GBPquote", reply(GBPdata, mycall, "sam"))) 
msg(JC . sam, JC . app, svcAns("GBPquote", reply(update(GBPdata, mycall,
    "sam"), badcall, "sam")))},ether(eee) > 
< JA : JVM | oCtr(0),
 {
< JA . csptk : AttackCSPTK | idle,lookup(JL . lup),fake("sam"),svcNames(
    "GBPquote" "USquote"),req(fakeCall),reply(none) >},ether(eee) >))

======================================================================
red findPath(st(eacf sjcf ljcf cjcf ajcf), prop1) .

reduce in MC1 : findPath(st(eacf sjcf ljcf ajcf cjcf), prop1) .
rewrites: 1060 in 70ms cpu (74ms real) (15142 rewrites/second)
result SimplePath: spath('ssptk.regreq 'jvm.new 'ssptk.sapId 'jvm.dispatch
    'attack.registerReq 'jvm.deliver 'ssptk.regreply 'ssptk.regreq 'jvm.new
    'ssptk.sapId 'jvm.dispatch 'attack.registerReq 'jvm.deliver 'ssptk.regreply
    'app.findsvc 'csptk.findServiceReq 'jvm.dispatch 'attack.lookupReq
    'jvm.deliver 'csptk.lookupOk 'jvm.new 'csptk.newidreply 'app.foundsvc
    'cssp.svcreq 'jvm.dispatch 'xmit.smsg 'jvm.deliver 'sssp.svcreq 'svc.svcreq
    'sssp.reply 'jvm.dispatch 'xmit.smsg 'jvm.deliver 'cssp.svcreply
    'app.svcans 'app.findsvc 'cssp.svcreq 'jvm.dispatch 'xmit.smsg 'jvm.deliver
    'sssp.svcreq 'svc.svcreq 'sssp.reply 'jvm.dispatch 'xmit.smsg 'jvm.deliver
    'cssp.svcreply 'app.svcans, st(
< eee : Attacker | inQ(none),outQ(none),clientIds(none),clientDs(none),pxDs(
    proxyD(CSP1, svc(JS . o(0))) proxyD(CSP1, svc(JS . o(1)))) > 
< JL : JVM | oCtr(0),
 {
< JL . lup : LOOKUP | svctable(none) >},ether(eee) > 
< JS : JVM | oCtr(2),
 {
< JS . GBPsvc : SVC | state(update(update(GBPdata, mycall, "sam"), badcall,
    "sam")) > 
< JS . USsvc : SVC | state(USdata) > 
< JS . ssptk : SSPTK1 | idle,lookup(JL . lup) > 
< JS . o(0) : SSP1 | idle,svc(JS . GBPsvc) > 
< JS . o(1) : SSP1 | idle,svc(JS . USsvc) > 
msg(JS . fred, JS . ssptk, registerReply) 
msg(JS . fred, JS . ssptk, registerReply)},ether(eee) > 
< JC : JVM | oCtr(1),
 {
< JC . csptk : CSPTK1 | idle,clientId("sam"),lookup(JL . lup) > 
< JC . app : APP | idle,svcFound(b("GBPquote", JC . o(0))),mytk(JC . csptk) > 
< JC . o(0) : CSP1 | idle,svc(JS . o(0)),clientId("sam") > 
msg(JC . sam, JC . app, svcAns("GBPquote", reply(GBPdata, mycall, "sam"))) 
msg(JC . sam, JC . app, svcAns("GBPquote", reply(update(GBPdata, mycall,
    "sam"), badcall, "sam")))},ether(eee) > 
< JA : JVM | oCtr(0),
 {
< JA . csptk : AttackCSPTK | idle,lookup(JL . lup),fake("sam"),svcNames(
    "GBPquote" "USquote"),req(fakeCall),reply(none) >},ether(eee) >))


)