LOGIC FOR VERIFYING PUBLIC-KEY CRYPTOGRAPHIC PROTOCOLS

A number of techniques based on logic theories have recently been deve loped to provide formal verification of security protocols. Many of th ese are based on logics of belief, which are considered useful in eval uating the trust which may be placed in a security protocol. Other tec hniques are based on logics of knowledge, which are suitable for provi ng protocol security. A new logic is proposed in the paper for formall y analysing public-key protocols. The logic, which combines the logics of knowledge and belief, enables the analysis of the security and tru stworthiness of a wide range of security protocols. Axioms are provide d which express the low level properties of public-key protocols. Thes e axioms can be combined, using inference rules, in attempting to dedu ce the desired goals for specific protocols. The paper presents the la nguage syntax for the logic, and a description of the axioms and infer ence rules. An example of the use of the new logic, in analysing a wel l known peer-entity authentication protocol, is also described.