*** attacker gets private data sent in call
search [1] (eacf ljcf sjcf cjcf) =>+ 
   ( cf:Configuration
    < eee : Attacker | atts:AttributeSet, clientDs(mycall cds:DataSet) > ) .

No solution.
states: 1722  rewrites: 16938 in 4450ms cpu (4500ms real) (3806
    rewrites/second)

*** attacker gets private data sent in reply (to query with private data)
search [1] (eacf ljcf sjcf cjcf) =>+ 
   ( cf:Configuration
    < eee : Attacker | atts:AttributeSet,
                       clientDs(reply(d:Data, mycall,"sam") cds:DataSet)> ) .
                    
No solution.
states: 1722  rewrites: 16938 in 4370ms cpu (4368ms real) (3875
    rewrites/second)

*** user gets answer from wrong service
search [1] (eacf ljcf sjcf cjcf1) =>+ 
   ( cf:Configuration
    < JC : JVM | jatts:AttributeSet,
      { cfig:Configuration
        < (JC . app) : APP | catts:AttributeSet,
                           todo(task("GBPquote", mycall) ts:Tasks),
                           waitfor(sid:Oid)  >
        msg(JC . app, sid:Oid, svcReply(reply(USdata, mycall, "sam")))
       }  > ) .

No solution.
states: 1076  rewrites: 10857 in 2740ms cpu (2733ms real) (3962
    rewrites/second)

*** user gets reply to non-permitted call to GBP
search [1] (eacf ljcf sjcf cjcf) =>+ 
   ( cf:Configuration
    < JC : JVM | jatts:AttributeSet,
      { cfig:Configuration
        < JC . app : APP | catts:AttributeSet,
                           todo(task("GBPquote", badcall) ts:Tasks),
                           waitfor(sid:Oid)  >
        msg(JC . app, sid:Oid, svcReply(reply(d:Data, badcall, "sam")))

       }  > )  such that initData(d:Data) == GBPdata .

No solution.
states: 1722  rewrites: 16938 in 4410ms cpu (4415ms real) (3840
    rewrites/second)

*** attacker gets reply with data for fakeId
*** don't really need good client
search [1] (eecf ljcf sjcf ajcf ) =>+ 
   ( cfx:Configuration    < JA : JVM | jatts:AttributeSet,
        { cf:Configuration
          < JA . app : APP | catts:AttributeSet,todo(ts:Tasks),
                             waitfor(sid:Oid) > 
       msg(JA . app, sid:Oid, svcReply(reply(d:Data, dc:Data, fakeId))) } > ) .

No solution.
states: 4590  rewrites: 41540 in 12040ms cpu (12097ms real) (3450
    rewrites/second)

*** doesn't terminate with cjcf included in initial state