Cryptographic protocols are usually specified in an informal language, with crucial elements of the protocol left implicit. We suggest that this is one reason that such protocols are difficult to analyse, and are subject to subtle and nonintuitive attacks. We present an approach for formalising and analysing cryptographic protocols in the situation calculus, in which all aspects of a protocol must be explicitly specified. We provide a declarative specification of underlying assumptions and capabilities, such that a protocol is translated into a sequence of actions to be executed by the principals, and a successful attack is an executable plan by an intruder that compromises the goal of the protocol. Our prototype verification software takes a protocol specification, translates it into a high-level situation calculus (Golog) program, and outputs any attacks that can be found. We describe the structure and operation of our prototype software, and discuss performance issues.
展开▼
