On BAN logic and hash functions or: How an unjustified inference rule causes problems

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.