15th IEEE Computer Security Foundations Workshop (CSFW'02)
Types and Effects for Asymmetric Cryptographic Protocols
Cape Breton, Nova Scotia, Canada
June 24-June 26
ISBN: 0-7695-1689-0
We present the first type and effect system for proving authenticity properties of security protocols based on asymmetric cryptography. The most significant new features of our type system are: (1) 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; (2) trust effects, to guarantee that tainted data does not,i n fact, originate from the opponent; and (3) challenge/response types to support a variety of idioms used to guarantee message freshness. We illustrate the applicability of our system via protocol examples.