A Logical Language for Specifying Cryptographic Protocol Requirements
NAVAL RESEARCH LAB WASHINGTON DC CENTER FOR HIGH ASSURANCE COMPUTING SYSTEMS (CHACS)
Pagination or Media Count:
In this paper we present a formal language for specifying and reasoning about cryptographic protocol requirements. We give examples of simple sets of requirements in that language. We look at two versions of a protocol that might meet those requirements and show how to specify them in the language of the NRL Protocol Analyzer. Mea91 Mea92 We also show how to map one of our 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. In other words, we use the Analyzer as a model checker to assess the validity of the formulae that make up the requirements.