Logic for verifying public-key cryptographic protocols

A number of techniques based on logic theories have recently been developed to provide formal verification of security protocols. Many of these are based on logics of belief, which are considered useful in evaluating the trust which may be placed in a security protocol. Other techniques are based on logics of knowledge, which are suitable for proving protocol security. A new logic is proposed in the paper for formally analysing public-key protocols. The logic, which combines the logics of knowledge and belief, enables the analysis of the security and trustworthiness of a wide range of security protocols. Axioms are provided which express the low level properties of public-key protocols. These axioms can be combined, using inference rules, in attempting to deduce the desired goals for specific protocols. The paper presents the language syntax for the logic, and a description of the axioms and inference rules. An example of the use of the new logic, in analysing a well known peer-entity authentication protocol, is also described.