Types and Effects for Asymmetric Cryptographic Protocols

Overview

This paper presents the first type and effect system for proving authenticity properties of security protocols based on asymmetric cryptography. The most significant new features of the type system are - a separation of public types (for data possibly sent to the opponent) from tainted types (for data possibly received from the opponent) via a subtype relation; trust effects, to guarantee that tainted data does not, in fact, originate from the opponent; and challenge/ response types to support a variety of idioms used to guarantee message freshness. The paper illustrates the applicability of the system via protocol examples.