BAN(P, X): trait
% BAN Logic, i.e. the logic presented in
%
% "A Logic of Authentication"
% SRC Research Report 39
% Michael Burrows, Martin Abadi, and Roger Needham.
% February 28, 1989
introduces
[ __ ] : X -> Bool % interpretation of modal statement
__ \also __ : X, X -> X % modal version of /\
__ \believes __: P, X -> X
__ \sees __: P, X -> X
__ \said __: P, X -> X
__ \controls __: P, X -> X
fresh: X -> X
sharedKey: K, P, P -> X
publicKey: K, P -> X
__ \inv: K -> K
secret: X, P, P -> X
encrypt: X, K, P -> X
__ \combine __: X, X -> X
hash: X -> X
send: P, P, X -> X
asserts
forall p,q,r: P, k: K, x,y: X
% send
([ send(p, q, x) ] => [ q \sees x ]);
% commutativity rules
secret(x, p, q) == secret(x, q, p);
sharedKey(k, p, q) == sharedKey(k, q, p);
% message-meaning rules
[p \believes sharedKey(k, q, p)] /\ [p \sees encrypt(x, k, r)] /\ p \neq r
=> [p \believes (q \said x)];
[p \believes publicKey(k, q)] /\ [p \sees encrypt(x, k \inv, r)] /\ p \neq r
=> [p \believes (q \said x)];
[p \believes secret(y, q, p)] /\ [p \sees (x \combine y)]
=> [p \believes (q \said x)];
% nonce-verification fule
[p \believes fresh(x)] /\ [p \believes (q \said x)]
=> [ p \believes (q \believes x) ];
% hmmm... x must be free of encrypt() terms
% jurisdiction rule
[p \believes (q \controls x)] /\ [p \believes (q \believes x)]
=> [p \believes x];
% \also \believes
[p \believes x] /\ [p \believes y]
=> [p \believes (x \also y)];
[p \believes (x \also y)]
=> [p \believes x];
[p \believes (x \also y)]
=> [p \believes y];
% \also \said
[p \believes (q \said (x \also y))]
=> [p \believes (q \said x)];
% \sees rules
[p \sees (x \also y)] => [p \sees x];
[p \sees (x \combine y)] => [p \sees x];
[p \believes sharedKey(k, q, p)] /\ [p \sees encrypt(x, k, r)] /\ p \neq r
=> [p \sees x];
[p \believes publicKey(k, p)] /\ [p \sees encrypt(x, k, r)] /\ p \neq r
=> [p \sees x];
[p \believes publicKey(k, q)] /\ [p \sees encrypt(x, k \inv, r)] /\ p \neq r
=> [p \sees x];
% \also \fresh
[p \believes fresh(x \also y)] => [p \believes fresh(x)];
% hash \fresh
[p \believes fresh(x)] => [p \believes fresh(hash(x))]
implies
AC(\also, X)