A logical language for specifying cryptographic protocolrequirements

A formal language is presented for specifying and reasoning about cryptographic protocol requirements. Examples of simple sets of requirements in that language are given. The authors examine two versions of a protocol that might meet those requirements and show how to specify them in the language of the NRL Protocol Analyzer. They also show how to map one of the sets of formal requirements to the language of the NRL Protocol Analyzer and use the Analyzer to show that one version of the protocol meets those requirements. The Analyzer is used as a model checker to assess the validity of the formulas that make up the requirement