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: It produces short and informative derivations which can reveal quite subtle protocol errors. However, despite quite a number of attempts, the semantics of BAN logic remain 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.
| Mads Dam |
| Associate Professor at SICS and
IMIT/KTH, Stockholm Visitor to the NICTA Formal Methods Program |
| Date: | Thu Nov 25 2004 |
| Time: | 1:30 to 2:30pm |
| Location: | Level 1 Seminar Room, CSE Bldg (K17), UNSW Kensington campus |
Last updated by tbourke at Thu Nov 25 11:02:58 2004 GMT+1100