Secrecy by typing in security protocols

We develop principles and rules for achieving secrecy properties in securit y protocols. Our approach is based on traditional classification techniques , and extends those techniques to handle concurrent processes that use shar ed-key cryptography. The rules have the form of typing rules for a basic co ncurrent language with cryptographic primitives, the spi calculus, They gua rantee that, if a protocol typechecks, then it does not leak its secret inp uts.