- The BAN Logic of Authentication
- : Introduction
- : Formal System
- : : Elements
- : : Syntax
- : : Inference Rules
- : Protocols
- : References, Sources, and Links

- BAN::=following,

Net-
Note BAN is not built on top of the normal propositional calculus.
In the MATHS system formulae can be defined and reasoned with
anyway by introducing the syntax and inference rules.
- Participant::Sets, people and systems sending messages and entertaining beliefs.
- Message::Sets, things that are sent and perhaps believed by participants.
- Belief::Sets, things that can be believed but are not always transmitable.
- |- (mb): Message==>Belief.
- Key::@(Message), a special message that is used to encrypt and decrypt messages..
- (mb)|- (kb): Key ==> Belief.
- encrypt::Message><Key->Message.

encrypt(X,K)=message X was encrypted by key K and sent by some one else. {X}[K]::=encrypt(X,K). - Public_Key::@(Key).
- Private_Key::@(Key).
- For K:Public_Key, /K ::Private_Key.
- (dick)|- (Public_private_keys): For K:Public_key, {{X}[/K]}[K] = X.
- nonce::Message=Number used ONCE.
- A nonce is a one time number used to identify a message. They can be sequence numbers or random numbers.

Messages can be concatenated with + to give a new message, The order in which this is done does not matter. - |- (concatenation): Abelian_semigroup(Message, (+)).
In the original papers concatenation is shown by a comma: {X,Y,Z,...}[K] ::Message= {X + Y + Z ... }[K]

- For A,B,C:Participant.
- For X,Y,Z:Message.
- For K,K1,K2:Key.
### Syntax

- believes::infix(Participant, Belief, Belief).

A believes X=A is entitled to believe X. - A|≡ X::= A believes X.
- said::infix(Participant, Message, Belief).
- A said K::=once upon a time, A used key K.
- A said X::=once upon a time, A said X.
- A|~X::=A said X.
- controls::infix(Participant, Message, Belief).

A controls X=A is an authority on X and can be trusted on X. - A |=> X::= A controls X.
- sees::infix(Participant, Message, Belief).

A sees X=Someone has sent a message to A containing X so that he can read X and repeat it. Implicitly in this: the message X is not sent to A by A itself! - A \triangleleft X::= A sees X.
- fresh::Message -> Belief.

fresh(X)=X has not been sent in a previous run of the protocol, Typically X contains time-stamp-like info identifying it as current from a relevant source. Many attacks use previously recorded messages to full the recipient into believing them. Freshness means that the information transmitted identifies itself as being current. - \sharp::=fresh.
- share(K)::infix(Participant, Message, Belief).

A share(K) B =A and B can use Key K to communicate. The key is known and used by A and B but nobody else will discover it and use it. - Shorthand form is a two-way double arrow with K on top.
- has_public_key::infix(Participant, Key, Belief).

B has_public_key K=B has a published public key K and has a private key /K. So B sends messages encrypted by /K but others use K to decrypt them. - Shorthand: An arrow with a vertical tail with K over it.
- secret(K)::infix(Participant, Message, Belief).

A secret(K) B=X is a secret known only to A, B and possibly some trusted associates. - Shorthand: looks like a chemical two way reaction -- two opposed harpoons with K over the top.
- combine::Message><Message->Message.
<X>[Y]::Message=message X combined with Y so that Y is a secret and identifies whoever sends the combined message.
### Inference Rules

- |- (message_meaning): If A believes(A share(K) B) and A sees {X}[K] then A believes(B said X).
- |- (public_key_message_meaning): If A believes(B has_public_key K) and A sees {X}[/K] then A believes(B said X).
- |- (secret_message_meaning): If A believes(A secret(K) B) and A sees <X>[K] then A believes(B said X).
- |- (nonce_verification): If A believes(fresh X) and A believes(B said X) then B believes X.
- |- (jurisdiction): If A believes(B controls X) and A believes (B believes X) then A believes X.
- |- (components_1): If A sees (X + Y ) then ((A sees X) and (A sees Y)).
- |- (components_2): If A believes (A share(K) B) and A sees {X}[K] then (A sees X).
- |- (components_3): If A sees <X>[Y] then (A sees X).
- |- (components_4): If A believes (B has_public_key K) and A sees {X}[/K] then (A sees X).
- |- (freshness_is_contagious): If A believes fresh(X) then A believes fresh(X + Y).
- |- (+out1): If A believes(X + Y) then (A believes X).
- |- (+out2): If A believes(X + Y) then (A believes Y).
- (dick)|- (+in): If A believes X and A believes Y then A believes (X + Y).
- (Anderson99)|- (key_meaning): If A believes(A share(K) B) and A sees {X}[K] then A believes(B said K).

The syntax shows both the long hand (readable) syntax and the shorthand (writable) mathematical symbols.

I (dick) have taken a few liberties in formalizing the logic such as separating messages from beliefs after some experiences with a partial implementation [ BAN.plg ] in Prolog.

### Elements

(End of Net BAN)

- protocol::=#message.
- message::=participant "->" participant ":" data eoln.
## References, Sources, and Links

- Abelian_semigroup::= See http://csci.csusb.edu/dick/maths/math_31_One_Associative_Op.html#abelian_semigroup.
- Anderson99::=following,
- Ross J Anderson
- The Formal Verification of a Payment System
- In HincheyBowen99 pp43-52

- BurrowsAbadiNeedham89::=following,
- M Burrows & M Abadi & R M Needham
- A Logic of Authentication
- Proc Royal Society of London A V426(1989)pp233-271
- Ref In [Anderson99]

- BurrowsAbadiNeedham90::=following,
- Michael Burrows & Martin Abadi & Roger M Needham
- A Logic of Authentication
- ACM Transactions on Computer Systems V8n1(Feb 1990)pp18-36 [ 77648.77649 ]

- dick::=Assertions I've added to the original presentation.
- infix::=A symbol or operator placed between two formulae to make another one. For Sets A,B,C, infix(A,B,C)= A><B->C.
- MATHS::= See http://csci.csusb.edu/dick/maths.

. . . . . . . . . ( end of section References, Sources, and Links) <<Contents | End>>

For more see Timo Kyntaja's page: [ ban.html ] , or Annette Bleeker and Lambert Meertens's [ http://dimacs.rutgers.edu/Workshops/Security/program2/bleeker/ ] paper on supplying a semantic model to the BAN logic. More web pages and Usenet discussions can be found easily on Google.

. . . . . . . . . ( end of section Formal System) <<Contents | End>>

. . . . . . . . . ( end of section The BAN Logic of Authentication) <<Contents | End>>