Cryptyc: Cryptographic Protocol Type Checking

The objectives of the Cryptyc project are to develop a Cryptographic Protocol Type Checker, which allows secrecy and authenticity properties of cryptographic protocols to be specified as types. A formal type soundness proof shows that any protocol which passes the type checker is guaranteed to satisfy its secrecy and authenticity requirements.

Prior work on the Cryptyc project has developed a theory and tool which deals with many, but not all, cryptographic techniques and attacker models. This project extends the Cryptyc system to include

support for more advanced cryptographic primitives, more sophisticated attacker models, object-based component architectures, and applies the Cryptyc system to the development of secure component libraries for cryptographic protocols.