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)