mod MC is
  inc SIMPLE .
  inc TEST-LOOKUP .

  op st : Configuration -> State .

  ops prop0 prop01 prop1 prop2 prop3 : -> 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 prop0 = true .

  eq  st(C:Configuration 
         < JC : JVM | jatts:AttributeSet,
           { jconf:Configuration
             msg(JC . sam, JC . app, svcAns(sn:String, d:Data)) } > )
      sat prop01 = true .


*** client accepts proxy to attacker svc
  eq st(cf:Configuration 
    < JC : JVM | atts:AttributeSet,
      { ocf:Configuration
        < O:Oid : CP0 | svc(JL . AttackSvc ), satts:AttributeSet >
       msg(JC . app, JC . csptk, findServiceOk(sn:String, O:Oid))
      } > ) 
    sat prop1 = true .

*** client accepts wrong proxy


  eq st( cf:Configuration 
    < JC : JVM | jcatts:AttributeSet,
      { ocf:Configuration
        < O:Oid : cl:Cid | svc(S:Oid), satts:AttributeSet >
       msg(JC . app, JC . csptk, findServiceOk(sn:String, O:Oid))
      } >
    < JL : JVM | jlatts:AttributeSet,
     {  locf:Configuration
       < (JL .  lup) : AttackerLookup |
          svctable(st:ServiceTable), latts:AttributeSet >
      } > 
    )
    sat prop2 = not(Registered(st:ServiceTable,sn:String,S:Oid)) 
 .

*** svc integrity violated

  eq st( cf:Configuration
    < JS : JVM | jsatts:AttributeSet,
     {  locf:Configuration < svc:Oid : SVC | state(sd:Data) > }
     > 
   )
   sat prop3 = hasUpdate(sd:Data,acall,fakeId)  .


endm

