any new form of analysis. Instead, it makes verification more accessible to the designers of protocols. Its key contribution is a new characterization of these protocols that is both closer to how designers conceive them, and amenable to a more direct encoding in standard first-order logic. This more direct encoding allows existing tools to be applied as black boxes without modification; it requires no tweaking of parameters or issuing of special directives by the user. Moreover, because the semantic gap between informal descriptions of protocols and their formalization is smaller, there are fewer opportunities for errors to creep in.

In this paper, the Alloy modeling language is used to record the details of the protocol and its security goals, and the Alloy Analyzer is used to find flaws. The approach, however, requires no special features of Alloy or its analysis, and could be applied in the context of any formal method based on first-order logic. Its simplicity suggests that it may be useful in teaching; indeed, using the approach, we have explained cryptographic protocols to undergraduates who have had only a few weeks of experience in formal methods.

Our approach, which we call [*knowledge flow analysis*]{}, gives a uniform framework 