Semantical investigations into BAN-like logics

Abstrakt:

BAN-logic is an epistemic logic for verification of security protocols proposed by Burrows, Abadi and Needham in the late 80'es. From a practical point of view, BAN logic has turned out to be quite successful: Reasoning about cryptographic protocol in terms of principals knowledge is arguably very natural, and moreover, BAN logic produces short and informative derivations which can reveal quite subtle protocol errors. However, despite quite a number of attempts, the semantics of BAN logic has remained problematic. In the talk we pinpoint the rule of normality, essentially monotonicity of the epistemic modality, as the chief culprit: This rule is validated by all proposed semantics we know of, but by adding it to BAN logic intuitively absurd statements become derivable from intuitively correct ones without much trouble. To overcome this problem we propose to adopt an idea from counterpart semantics, namely to generalize the epistemic accessibility relation from a relation between local states to a relation between pairs of messages and local states, by systematically renaming content which is cryptographically inaccessible. We use this idea to build a new semantics for BAN logic which we claim avoids the problems of the previous semantics, and we show how the idea can be used to build semantics for richer logics up to and including first-order BAN logic. The latter is interesting, in particular, since it provides a framework in which existing semantics can be compared. Finally, if there is time, we will discuss soundness of the proposed cryptographic counterpart semantics.