---

pa(e) ==
  let n,v = pa in
    if n =a "new" then (e  New)  (New(e) = v)
   if n =a "send" then (e  Send)  (Send(e) = v)
   if n =a "rcv" then (e  Rcv)  (Rcv(e) = v)
   if n =a "encrypt" then (e  Encrypt)  (Encrypt(e) = v)
   if n =a "decrypt" then (e  Decrypt)  (Decrypt(e) = v)
   if n =a "sign" then (e  Sign)  (Sign(e) = v)
   if n =a "verify" then (e  Verify)  (Verify(e) = v)
   else False
   fi 

---

Definitions :  spread: spread def,  ses-new: New,  ses-send: Send,  ses-rcv: Rcv,  ses-encrypt: Encrypt,  encryption-key: Key,  ses-decrypt: Decrypt,  ses-sign: Sign,  ifthenelse: if b then t else f fi ,  eq_atom: x =a y,  token: "$token",  and: P  Q,  assert: b,  in-eclass: e  X,  equal: s = t,  sdata: SecurityData,  product: x:A  B[x],  Id: Id,  atom: Atom$n,  eclass-val: X(e),  ses-verify: Verify,  false: False
FDL editor aliases :  is-p-act

---

pa(e)  ==
    let  n,v  =  pa  in
        if  n  =a  "new"  then  (\muparrow{}e  \mmember{}\msubb{}  New)  \mwedge{}  (New(e)  =  v)
      if  n  =a  "send"  then  (\muparrow{}e  \mmember{}\msubb{}  Send)  \mwedge{}  (Send(e)  =  v)
      if  n  =a  "rcv"  then  (\muparrow{}e  \mmember{}\msubb{}  Rcv)  \mwedge{}  (Rcv(e)  =  v)
      if  n  =a  "encrypt"  then  (\muparrow{}e  \mmember{}\msubb{}  Encrypt)  \mwedge{}  (Encrypt(e)  =  v)
      if  n  =a  "decrypt"  then  (\muparrow{}e  \mmember{}\msubb{}  Decrypt)  \mwedge{}  (Decrypt(e)  =  v)
      if  n  =a  "sign"  then  (\muparrow{}e  \mmember{}\msubb{}  Sign)  \mwedge{}  (Sign(e)  =  v)
      if  n  =a  "verify"  then  (\muparrow{}e  \mmember{}\msubb{}  Verify)  \mwedge{}  (Verify(e)  =  v)
      else  False
      fi 


Date html generated: 2010_08_28-AM-03_11_56
Last ObjectModification: 2010_02_23-AM-01_30_06

Home Index