Types and effects for asymmetric cryptographic protocols

Issue title: Special issue on CSFW15

Guest editors: S. Schneider

Article type: Research Article

Authors: Gordon, Andrew D.^a | Jeffrey, Alan^{b; 1; *}

Affiliations: [a] Microsoft Research, Microsoft Corporation, One Microsoft Way, Redmond, WA 98052, USA | [b] CTI, DePaul University, 243 S. Wabash Ave., Chicago, IL 60604, USA

Correspondence: [*] Corresponding auhor. E-mail: ajeffrey@cs.depaul.edu.

Note: [1] This material is based upon work supported by the National Science Foundation under Grant No. 0208549.

Abstract: 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.

DOI: 10.3233/JCS-2004-123-406

Journal: Journal of Computer Security, vol. 12, no. 3-4, pp. 435-483, 2004