Scribd Logo
Upload

Welcome to Scribd!

  • 25 views

    BAN Logic A Logic of Authentication: Sape J. Mullender

    Uploaded by

    wind_art
    The document summarizes the BAN logic, which is a logic of belief and action developed by Mike Burrows, Martín Abadi, and Roger Needham. It provides notation for expressing beliefs and messages in authentication protocols. The logic can be used to analyze authentication protocols and determine whether they achieve their goals, though it cannot prove protocols flawed. Examples of analyzing the Ottway-Rees and Needham-Schroeder authentication protocols using BAN logic are provided.

    Copyright:

    Attribution Non-Commercial (BY-NC)
    Download as PDF, TXT or read online from Scribd

    BAN Logic A Logic of Authentication: Sape J. Mullender

    Uploaded by

    wind_art
    25 views23 pages
    The document summarizes the BAN logic, which is a logic of belief and action developed by Mike Burrows, Martín Abadi, and Roger Needham. It provides notation for expressing beliefs and messages in authentication protocols. The logic can be used to analyze authentication protocols and determine whether they achieve their goals, though it cannot prove protocols flawed. Examples of analyzing the Ottway-Rees and Needham-Schroeder authentication protocols using BAN logic are provided.

    Original Description:

    Protocol analysis

    Original Title

    Ban

    Copyright

    © Attribution Non-Commercial (BY-NC)

    Available Formats

    PDF, TXT or read online from Scribd

    Did you find this document useful?

    Is this content inappropriate?

    The document summarizes the BAN logic, which is a logic of belief and action developed by Mike Burrows, Martín Abadi, and Roger Needham. It provides notation for expressing beliefs and messages in authentication protocols. The logic can be used to analyze authentication protocols and determine whether they achieve their goals, though it cannot prove protocols flawed. Examples of analyzing the Ottway-Rees and Needham-Schroeder authentication protocols using BAN logic are provided.

    Copyright:

    Attribution Non-Commercial (BY-NC)
    Download as PDF, TXT or read online from Scribd
    Download as pdf or txt
    25 views23 pages

    BAN Logic A Logic of Authentication: Sape J. Mullender

    Uploaded by

    wind_art
    The document summarizes the BAN logic, which is a logic of belief and action developed by Mike Burrows, Martín Abadi, and Roger Needham. It provides notation for expressing beliefs and messages in authentication protocols. The logic can be used to analyze authentication protocols and determine whether they achieve their goals, though it cannot prove protocols flawed. Examples of analyzing the Ottway-Rees and Needham-Schroeder authentication protocols using BAN logic are provided.

    Copyright:

    Attribution Non-Commercial (BY-NC)
    Download as PDF, TXT or read online from Scribd
    Download as pdf or txt
    You are on page 1of 23

    BAN Logic A Logic of Authentication

    Sape J. Mullender
    Huygens Systems Research Laboratory Universiteit Twente Enschede

    BAN Logic

    The BAN logic was named after its inventors, Mike Burrows, Mart Abad and Roger Needham. n , The logic is, as they stated, a logic of belief and action. It contains no logical inversions; therefore it cannot be used to prove a protocol awed. But when proof that a protocol is correct cannot be obtained, that protocol deserves to be treated with grave suspicion.

    Notation
    The logic reasons about beliefs. If Alice believes a proposition P , we write A | P and say A believes P . Alice believes that KAT is a good key for communicating with Trent. This is expressed as A | A T ; we say A believes KAT is a good key for A and T . Trent acts as authentication server or certication authority in many of the protocols analyzed by BAN logic. If Alice believes that Trent can be trusted to create a good key for K communication with Bob, we write A | T A B; we say A believes T has jurisdiction over or speaks for good keys for A and B.
    3

    KAT

    Messages

    When Alice receives a message (which, in our logic, always contains a proposition), we write A P and say A sees P . Seeing is not believing unless you know who said it. Note that, in this logic, nobody says anything he or she does not believe. If Alice sent a message containing the statement P , we may write A | P and say A once said P . But, Alice may have said it so long ago that we can no longer trust the contents of her message. We need to know that Alices statement is fresh. When a statement P is fresh we write #(P ) and say P is fresh.

    Notation Summary

    P | X P X P | X #(P ) P X P Q P P Q X Y
    X K K

    P P P P P

    believes X sees X once said X is fresh has jurisdiction over X

    K is a good key for communicating between P and Q P has K as a public key X is a secret known only to P and Q X combined with (secret) Y

    Axioms

    We adopt the notation in the BAN papers: then Q is true.

    P Q

    means if P is true

    We assume that participants in protocols are good logicians: if Alice believes a proposition X and X , then she believes Y Y too. This is true for the axioms also.

    Message meaning rules

    P | P Q, P {X}K P | Q | X P | Q, P {X}K 1 P | Q | X P | P Q, P X P | Q | X
    Y Y K

    Nonce Verication

    P | #(X) , P | Q | X P | Q | X

    Jurisdiction Rule

    P | Q X, P | Q | X P | X

    More Rules

    P | X, P | Y P | (X, Y ) P | (X, Y ) P | X P | Q | (X, Y ) P | Q | X P | Q | (X, Y ) P | Q | X

    10

    And More

    (X, Y ) P X X Y) X {X}K

    P P
    K

    P | P Q, P P X

    11

    And More

    P | P , P P X
    K

    {X}K

    P | Q, P {X}K 1 P X P | #(X) A | #((X, Y ))

    12

    Analysis of Protocols

    Most analyses start with assumptions such as A | A T A | T A B A | #(NA) T | A B and need to conclude with KAB KAB A | A B B | A B A | B | A B
    KAB KAB KAB KAT

    B | B T B | T B B B | #(NB )
    KAB

    KBT

    B | A | A B

    KAB

    13

    The Ottway-Rees Authentication Protocol

    1. 2. 3. 4.

    M, A, B, {NA, M, A, B}KAT M, A, B, {NA, M, A, B}KAT , {NB , M, A, B}KBT M, {NA, KAB }KAT , {NB , KAB }KBT M, {NA, KAB }KAT

    14

    Analysis The Protocol

    1.

    M, A, B, {NA, M, A, B}KAT {NA, NC }KAS M, A, B, {NA, M, A, B}KAT , {NB , M, A, B}KBT {NA, NC }KAS , {NB , NC }KBS M, {NA, KAB }KAT , {NB , KAB }KBT {NA, A B, B | NC }KAT , {NB , A B, A | NC }KBT
    KAB KAB

    2.

    3.

    4.

    M, {NA, KAB }KAT {NA, A B, B | NC }KAT


    KAB

    15

    Analysis Assumptions

    A | A T T | A T T | A B A A A A | | | | T A B T B | X #(NA) #(NC )
    KAB KAB KAT

    KAT

    B | B T T | B T B | T B B B | T A | X B | #(NB )
    KAB KBT

    KBT

    16

    Analysis Derivations
    KAB KBT

    {NB , A B}KBT , B | B T B | T | NB , A B
    KAB

    {NB , A B}KBT , B | #(NB ) B | #(A B)


    KAB

    KAB

    B | T | A B, B | #(A B) B | T | A B B | T | A B, B | T A B B | A B
    KAB KAB KAB KAB

    KAB

    KAB

    17

    Analysis Conclusion

    Similarly, we derive A | A B. We can also derive A | B | NC , but we can only prove B | A | NC . NA is not needed, NC can be used instead.

    KAB

    18

    the Needham-Schroeder Protocol

    1. 2. 3. 4. 5.

    A, B, NA {NA, B, KAB , {A, KAB }KBT }KAT {A, KAB }KBT {NB }KAB {NB 1}KAB

    19

    Needham-Schroeder Analysed

    Assumptions: T | A B A | A T T | A T A | T A B A | T #(KAB ) A | #(NA) T | #(KAB )


    KAB KAT KAT KAB

    B | B T T | B T B | T B B B | #(NB ) B | #(A B)
    K KAB KBT

    KBT

    20

    Messages

    1. 2.

    A, B, NA {NA, B, KAB , {A, KAB }KBT }KAT {NA, A B, #(A B) , {A B}KBT }KAT
    KAB KAB KAB

    3.

    {A, KAB }KBT {A B}KBT


    KAB

    4.

    {NB }KAB {NB , A B}KAB f r omB


    KAB

    5.

    {NB 1}KAB {NB , A B}KAB f r omA


    KAB

    21

    Analysis

    As in the Ottway-Rees protocol, we have the message for Alice saying {NA, A B}KAT , so we can prove in an identical manner A | A B. But Bob gets no message linking Trents statement A B to something he knows to be fresh. We cannot get beyond B | T | A B.
    KAB KAB KAB KAB

    22

    Needham-Schroeder Exposed

    This exactly puts the nger on the weakness in the NeedhamSchroeder protocol: Mallory could record Alice and Bobs key exchange and trick Bob into accepting the key in Message 3 any time he chooses. Mallory will be thwarted, however, when he cannot respond to Bobs Message 4. But if he can aord to spend a year of CPU time cracking KAB , he can get Bob to accept and use a year-old key.

    23

    You might also like