Title :
Exploring the BAN approach to protocol analysis
Author :
Snekkenes, Einar
Author_Institution :
Alcatel Telecom Norway AS, Oslo, Norway
Abstract :
The BAN approach to analysis of cryptographic protocols (M. Burrows et al., 1988) transforms a correctness requirement into a proof obligation of a formal belief logic. It is shown that the BAN protocol annotation rules make flaws due solely to protocol step permutation undetectable by the BAN logic. This is illustrated by a short example. In the style of BAN logic, the author defines the concept of a terminating idealized protocol. BAN logic has been used to prove the correctness of an insecure protocol (D. Nessett, 1990). The author shows that this protocol belongs to the class of nonterminating protocols
Keywords :
cryptography; formal logic; protocols; BAN logic; BAN protocol; computer security; cryptographic protocols; formal belief logic; insecure protocol; nonterminating protocols; protocol analysis; terminating idealized protocol; Algorithm design and analysis; Authentication; Body sensor networks; Cryptographic protocols; Information analysis; Information security; Logic; Plasma welding; Protection; Telecommunications;
Conference_Titel :
Research in Security and Privacy, 1991. Proceedings., 1991 IEEE Computer Society Symposium on
Conference_Location :
Oakland, CA
Print_ISBN :
0-8186-2168-0
DOI :
10.1109/RISP.1991.130785
