---
abstract: 'Knowledge flow analysis offers a simple and flexible way to find flaws in security protocols. A protocol is described by a collection of rules constraining the propagation of knowledge amongst principals. Because this characterization corresponds closely to informal descriptions of protocols, it allows a succinct and natural formalization; because it abstracts away message ordering, and handles communications between principals and applications of cryptographic primitives uniformly, it is readily represented in a standard logic. A generic framework in the Alloy modelling language is presented, and instantiated for two standard protocols, and a new key management scheme.'
author:
- |
    Emina Torlak, Marten van Dijk, Blaise Gassend, Daniel Jackson, and Srinivas Devadas\
    {emina, marten, gassend, dnj, devadas}@mit.edu
---

Introduction
============

One area of major successes for formal methods has been the verification of security protocols. A number of specialized tools have been developed in the last decade that have exposed subtle flaws in existing protocols (see, e.g. [@Lowe97; @CJM00]). For the most part, however, these tools have been used by the researchers that developed them, and less attention has been paid to usability issues.

This paper presents a new approach to formulating and checking cryptographic protocols. It does not enable 