---

UsedAtoms(e) ==
  if e  Send then sdata-atoms(Send(e))
  if e  Sign then sdata-atoms(signed(e))
  if e  Verify then [signature(e) / sdata-atoms(signed(e))]
  if e  Encrypt then sdata-atoms(plainText(e)) @ encryption-key-atoms(key(e))
  if e  Decrypt then [cipherText(e) / encryption-key-atoms(key(e))]
  else []
  fi 

---

Definitions :  eclass-val: X(e),  ses-send: Send,  ses-sign: Sign,  ses-signed: signed(e),  ses-verify: Verify,  ses-verify-sig: signature(e),  ses-verify-signed: signed(e),  ses-encrypt: Encrypt,  append: as @ bs,  sdata-atoms: sdata-atoms(d),  ses-encrypted: plainText(e),  ses-encryption-key: key(e),  ifthenelse: if b then t else f fi ,  in-eclass: e  X,  ses-decrypt: Decrypt,  cons: [car / cdr],  ses-cipher: cipherText(e),  encryption-key-atoms: encryption-key-atoms(k),  ses-decryption-key: key(e),  nil: []
FDL editor aliases :  ses-used-atoms

---

UsedAtoms(e)  ==
    if  e  \mmember{}\msubb{}  Send  then  sdata-atoms(Send(e))
    if  e  \mmember{}\msubb{}  Sign  then  sdata-atoms(signed(e))
    if  e  \mmember{}\msubb{}  Verify  then  [signature(e)  /  sdata-atoms(signed(e))]
    if  e  \mmember{}\msubb{}  Encrypt  then  sdata-atoms(plainText(e))  @  encryption-key-atoms(key(e))
    if  e  \mmember{}\msubb{}  Decrypt  then  [cipherText(e)  /  encryption-key-atoms(key(e))]
    else  []
    fi 


Date html generated: 2010_08_28-AM-02_41_27
Last ObjectModification: 2010_02_22-PM-11_12_12

Home Index