Security of communication in modern applications is an increasingly important issue. Although there are strong cryptographic techniques, security is often broken nevertheless due to weaknesses in the implementation or in the exchange protocols. Advances in verification and theorem-proving techniques have led to techniques for encapsulating proofs of properties in the type of a program, leading to programs that, by typing alone, satisfy certain properties. This paper extends such techniques to affine logics, which are resource aware, that is, where the number of times information is used can be restricted. This can help prevent, for example, man-in-the-middle attacks.

The paper starts with a general overview of the techniques of refinement types (dependent type packaging a type with a logical formula expressing properties of the values of the type). Some motivating examples illustrate that current techniques cannot easily capture bounds on resource usage.

The following sections introduce the resource aware logic (affine logic) chosen as the basis for the later techniques, together with some key definitions and theorems. Next, the functional programming system RCF is extended by constructs and a type system based on affine logic and some basic properties of this formalism are proved.

The third part of the paper presents a basic protocol library based on this system and analyzes two existing security protocols (EPMO and Kerberos) with the tools previously defined.

The paper closes with a detailed analysis of type checking containing the structure of an algorithm for type checking. Finally, the usual overview of related work is given. Several appendices contain detailed proofs of several formal results stated in the paper.

The paper is well structured, very thorough, and detailed, while still a good read.