Title :
Decision procedures for the analysis of cryptographic protocols by logics of belief
Author_Institution :
ENS-LIENS, Ecole Normale Superieure, Paris, France
Abstract :
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
Keywords :
belief maintenance; cryptography; program verification; protocols; BAN logic; belief-logic deductions; completeness; cryptographic protocols; decision procedures; forward-chaining algorithm; logics of belief; protocol security logics; termination; Body sensor networks; Computer science; Credit cards; Cryptographic protocols; Cryptography; IP networks; Laboratories; Logic; Security; Termination of employment;
Conference_Titel :
Computer Security Foundations Workshop, 1999. Proceedings of the 12th IEEE
Conference_Location :
Mordano
Print_ISBN :
0-7695-0201-6
DOI :
10.1109/CSFW.1999.779761