Models and Proofs of Protocol Security
Source: University of California
As computer security has become a broad, rich field, rigorous models have been developed for many policies and mechanisms. Sometimes these models have been the subject of formal proofs, even automated ones. The goal of this paper is to discuss some of the progress in this direction and some of the problems that remain. The paper focuses on the study of security protocols, a large, mature, and active area. It aims to offer an introduction and a partial perspective on this area, rather than a comprehensive survey. The authors explain notations, results, and tools informally, through the description of a basic example: a variant of the classic Wide-mouthed-frog protocol.