Decision Procedures for the Analysis of Cryptographic Protocols by Logics of Belief

Belief-logic deductions are used in the analysis of cryptographic protocols. We show a new method to decide such logics. In addition to the familiar BAN logic, it is also applicable to the more advanced versions of protocol security logics, and GNY in particular; and it employs an efficient forward-chaining algorithm the completeness and termination of which are proved. Theoretic proofs, implementation decisions and results are discussed.

• Type: Conference
• Year: 1999
• Where: CSFW
• Authors: David Monniaux
• Keywords: CSFW 1999, Efficient Forward-chaining Algorithm, Familiar Ban Logic, Protocol Security Logics, Security Privacy