---

ProtocolAction ==
  n:Atom  if n =a "new" then Atom1
           if n =a "send" then SecurityData
           if n =a "rcv" then SecurityData
           if n =a "encrypt" then SecurityData  Key  Atom1
           if n =a "decrypt" then SecurityData  Key  Atom1
           if n =a "sign" then SecurityData  Id  Atom1
           if n =a "verify" then SecurityData  Id  Atom1
           else Top
           fi 

---

Definitions :  atom: Atom,  encryption-key: Key,  ifthenelse: if b then t else f fi ,  eq_atom: x =a y,  token: "$token",  sdata: SecurityData,  product: x:A  B[x],  Id: Id,  atom: Atom$n,  top: Top
FDL editor aliases :  p-act

---

ProtocolAction  ==
    n:Atom  \mtimes{}  if  n  =a  "new"  then  Atom1
                      if  n  =a  "send"  then  SecurityData
                      if  n  =a  "rcv"  then  SecurityData
                      if  n  =a  "encrypt"  then  SecurityData  \mtimes{}  Key  \mtimes{}  Atom1
                      if  n  =a  "decrypt"  then  SecurityData  \mtimes{}  Key  \mtimes{}  Atom1
                      if  n  =a  "sign"  then  SecurityData  \mtimes{}  Id  \mtimes{}  Atom1
                      if  n  =a  "verify"  then  SecurityData  \mtimes{}  Id  \mtimes{}  Atom1
                      else  Top
                      fi 


Date html generated: 2010_08_28-AM-02_46_08
Last ObjectModification: 2010_02_23-AM-12_13_56

Home Index