load new-all.m
load model-checker
load ../ALL/simple.m
load ../ALL/mc.m

mod MC1 is
  inc MC .
  inc SPTK1-TEST .

endm

***(

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

 red findPath(st(icf),prop1) .
reduce in MC1 : findPath(st(icf), prop1) .
rewrites: 1064 in 120ms cpu (118ms real) (8866 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, 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(CSP1, svc(JS . o(0))) proxyD(CSP1,
    svc(JS . o(1)))),attackeeSet(proxyD(CSP1, svc(JS . o(0))) proxyD(CSP1, svc(
    JS . o(1)))),myCPTK(JL . csptk),myPxd(proxyD(CP0, svc(JL . AttackSvc))),
    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(GBPdata) > 
< 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 : 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 MC1 : findPath(st(icf), prop2) .
rewrites: 1088 in 80ms cpu (78ms real) (13600 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, 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(CSP1, svc(JS . o(0))) proxyD(CSP1,
    svc(JS . o(1)))),attackeeSet(proxyD(CSP1, svc(JS . o(0))) proxyD(CSP1, svc(
    JS . o(1)))),myCPTK(JL . csptk),myPxd(proxyD(CP0, svc(JL . AttackSvc))),
    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(GBPdata) > 
< 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 : 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 MC1 : findPath(st(icf), prop3) .
rewrites: 1071 in 80ms cpu (76ms real) (13387 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 : SSPTK1 | 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) >))


)