Types and Effects for Asymmetric Cryptographic Protocols

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, in 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. 1 Motivation In recent work [GJ03, GJ01], we propose a type-based methodology for checking authenticity properties of security protocols. First, specify properties by annotating an executable description of a protocol with correspondence assertions [WL93]. Second, annotate the protocol with suitable types. Third, verify the assertions by running a typechecker. A type-c...

• Type: Conference
• Year: 2002
• Where: CSFW
• Authors: Andrew D. Gordon, Alan Jeffrey
• Keywords: Asymmetric Cryptography, Authenticity Properties, CSFW 2002, Security Privacy, Security Protocols