An alternate explanation of two BAN-logic “failures”

Abstract

Boyd and Mao (“On a Limitation of BAN Logic”, in these proceedings) suggest that it is easy to use the authentication logic of Burrows, Abadi and Needham to approve protocols that are in practice unsound, and present two examples. We illustrate that the problem in the first example can be traced to a violation of pre-conditions in the BAN analysis (involving ill-founded trust in a trusted server), while in the second the idealization is simply incorrect. For the latter, a general guideline is proposed to avoid similar problems in the future.