Secrecy types for asymmetric communication

Abstract

We develop a typed process calculus for security protocols in which types convey secrecy properties. We focus on asymmetric communication primitives, especially on public-key encryption. These present special dificulties, partly because they rely on related capabilities (e.g., “public” and “private” keys) with different levels of secrecy and scopes.