On BAN logic and hash functions or: how an unjustified inference rule causes problems |
| |
Authors: | Wouter Teepe |
| |
Affiliation: | (1) Department of Computer Science, Digital Security group, Radboud University Nijmegen, Postbus 9010, 6500 GL Nijmegen, The Netherlands |
| |
Abstract: | BAN logic, an epistemic logic for analyzing security protocols, contains an unjustifiable inference rule. The inference rule
assumes that possession of H(X) (i.e., the cryptographic hash value of X) counts as a proof of possession of X, which is not the case. As a result, BAN logic exhibits a problematic property, which is similar to unsoundness, but not
strictly equivalent to it. We will call this property ‘unsoundness’ (with quotes). The property is demonstrated using a specially
crafted protocol, the two parrots protocol. The ‘unsoundness’ is proven using the partial semantics which is given for BAN logic. Because of the questionable character
of the semantics of BAN logic, we also provide an alternative proof of ‘unsoundness’ which we consider more important. |
| |
Keywords: | BAN logic Soundness Two parrots protocol Cryptographic hash function Security protocol |
本文献已被 SpringerLink 等数据库收录! |
|