*** security and trust mgt
***load stm.m
*** Security&TrustManager Class
fmod STM-IFACE is
  inc JCONF .
  inc STRING .
  inc DATA .
  sorts Policy Key Cred Permissions .

  op getId : Permissions -> String .     
  op  checkClientReq : String Cred -> MsgBody .
  op  checkClientReply : Permissions -> MsgBody .
  op  clientPerm : String Cred Policy -> Permissions .

  op  signReq : Data -> MsgBody .
  op  signReply : Data -> MsgBody .
  op  signed : Data  Key -> Data .

  op  verifySigReq : Data Key -> MsgBody .
  op  verifySigOk : Data -> MsgBody .
  op  verifySigFail : -> MsgBody .

  op  encryptReq : Data Cred -> MsgBody .
  op  encryptReply : Data -> MsgBody .
  op  encrypted : Data Key -> Data .

  op  decryptReq : Data -> MsgBody .
  op  decryptReply : DataX -> MsgBody .
endfm

fmod STM-CLASS is
  inc STM-IFACE .
  op STM : -> Cid .
  ops pkey skey : Key -> Attribute .
  op policy : Policy -> Attribute .
endfm

*** Security&Trust manager behavior
mod STM is
  inc STM-CLASS .

  op  keyPair : Key Key -> Bool [comm] .
  op  keyInv : Key -> Key .
  op  getKey : Cred -> Key .
  eq  keyPair(k1:Key, k2:Key) = (k2:Key == keyInv(k1:Key)) .

  op checkSig :  Data Key -> Bool .
  eq checkSig(signed(d:Data,k:Key), pk:Key) = keyPair(k:Key, pk:Key) .
  eq checkSig(d:Data, pk:Key) = false [owise] .

  op unSign :  Data -> Data .
  eq unSign(signed(d:Data,k:Key)) = d:Data .

  op  unencrypt : Data Key -> Data .
  eq  unencrypt(encrypted(d:Data,pk:Key), sk:Key)
      = if keyPair(sk:Key, pk:Key)
        then d:Data
        else badData 
        fi .

  rl[stm.sign]:
  < O:Oid : STM | pkey(pk:Key), skey(sk:Key), policy(p:Policy) >
  msg(O:Oid, C:Oid, signReq(x:Data))
  => 
  < O:Oid : STM | pkey(pk:Key), skey(sk:Key), policy(p:Policy) >
  msg(C:Oid, O:Oid, signReply(signed(x:Data,sk:Key))) .

  rl[stm.verify]:
  < O:Oid : STM | pkey(pk:Key), skey(sk:Key), policy(p:Policy) >
  msg(O:Oid, C:Oid, verifySigReq(d:Data, spk:Key))
  => 
  < O:Oid : STM | pkey(pk:Key), skey(sk:Key), policy(p:Policy) >
  if (checkSig(d:Data, spk:Key))
  then msg(C:Oid, O:Oid, verifySigOk(unSign(d:Data)) )
  else  msg(C:Oid, O:Oid, verifySigFail) 
  fi .

  rl[stm.checkCred]:
  < O:Oid : STM | pkey(pk:Key), skey(sk:Key), policy(p:Policy) >
  msg(O:Oid, P:Oid, checkClientReq(sn:String, ccred:Cred))
  => 
  < O:Oid : STM | pkey(pk:Key), skey(sk:Key), policy(p:Policy) >
  msg(P:Oid, O:Oid, 
      checkClientReply(clientPerm(sn:String,ccred:Cred,p:Policy)))  .

  rl[stm.encrypt]:
  < O:Oid : STM | pkey(pk:Key), skey(sk:Key), policy(p:Policy) >
  msg(O:Oid, P:Oid, encryptReq(d:Data, ccred:Cred))
  => 
  < O:Oid : STM | pkey(pk:Key), skey(sk:Key), policy(p:Policy) >
  msg(P:Oid, O:Oid, encryptReply(encrypted(d:Data,getKey(ccred:Cred)))) .

  rl[stm.decrypt]:
  < O:Oid : STM | pkey(pk:Key), skey(sk:Key), policy(p:Policy) >
  msg(O:Oid, P:Oid, decryptReq(d:Data))
  => 
  < O:Oid : STM | pkey(pk:Key), skey(sk:Key), policy(p:Policy) >
   msg(P:Oid, O:Oid, decryptReply(unencrypt(d:Data, sk:Key))) .
endm

