Secrecy types for a simulatable cryptographic library
Peeter Laud · 2005
We present a type system for checking secrecy of messages handled by protocols that use the Backes-Pfitzmann-Waidner library for cryptographic operations. A secure realization of this library exists, therefore we obtain for the first time a cryptographically sound analysis for a full language for expressing protocols, particularly handling symmetric encryption and unbounded number of sessions. The language is similar to the spi-calculus, but has a completely deterministic semantics. The type system is similar to the Abadi-Blanchet type system for asymmetric communication.