DOC PREVIEW
PSU CSE 543 - BAN Logic

This preview shows page 1 out of 2 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 2 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 2 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

CSE543/Fall 2006 - Homework Questions - BAN LogicDue: Tuesday, September 26, 2006 — Professor Trent JaegerPlease read the instructions and questions carefully. You will be graded for clarity and correctness.Short Answer - some will be one or two words – no more than 3 sentences1. (3pts) What is the goal of authentication protocol analysis?answer: To show that the two legitimate parties in an authentication protocol believe that only theother party shares a secret with them as the result of executing the protocol. The threat model isthat of a powerful attacker.2. (3pts) Use the logical postulates in BAN Logic (name them as they are used) to show that ”B believesA believes Nb” based on the following input knowledge:(i) B believes fresh(Nb)(ii) B sees {Nb}K−1(iii) B believes K−→Aanswer: (ii),(iii) implies (4) B believes A said Nbby Message Meaning Rule.(i),(4) implies (5) B believes A believes Nbby Nonce Verification Rule.Long Answer - no more than 2 paragraphs4. (7pts) Why is modeling attacker behavior one of the biggest challenges in protocol analysis? Howwell does B AN Logic address this challenge? Support your argument with BAN Logic conce pts.answer: A powerful attacker can eavesdrop, add any message, or modify any message. Thus, anattacker’s impact may be seen anywhere in protocol analysis.While the BAN Logic enables specification of messages seen (sees) and sent (said) among principals,it does not explicitly model attacker behavior nor search the space of attacker steps.5. (7pts) How does BAN Logic enable us to state our trust in an authentication server in Kerberosshared key? How does BAN Logic distinguish between trust in principals and the current state ofthe protocol?answer: In BAN Logic, we use the believes statement to specify our trust in what the participantshave at the start. However, trust that these cannot be leaked to attackers somehow is implicit.Distinguishing between trust and the protocol execution is implicit. Some state changes occur due torules in the logic, and some to the introduction of new facts during protocol execution. For example,when a subject chooses a nonce as part of the protocol, believes statements are used to indicate this.This could be considered as trust in the choice of the nonce or a protocol state change.Constructions - take your time and answer clearly and completely.6. (10pts) Gavin Lowe found a vulnerability in the Needham-Schroeder Public Key Protocol that was(supposedly) proven correct using the BAN logic in Section 6.The flaw enables an intruder I to trick principal B into believing that it shares a se cre t with A onlywhen it also shares this secret with I.The attack involves the intruder interleaving two sessions X (A authenticates to I correctly) and Y(I authenticates to B as A) in the manner below (using the notation in the paper where KXis thepublic key of X).1X.1 A → I {Na, A}KIY.1 I → B {Na, A}KBY.2 B → I {Nb, Na}KAX.2 I → A {Nb, Na}KAX.3 A → I {Nb}KIY.3 I → B {Nb}KB(a) Which of the final beliefs in the BAN logic proof (in the paper) is incorrect?(b) What rule is used to prove this belief (i.e., the one the generates these kinds of statements)?(c) Which precondition clause in that rule is not actually true?(d) How did the conclusion that only A and B know Naand Nbget proven when it is also pos siblefor I to know these values?answer: (a) B believes A believes Na(B believes that I has Na)(b) nonce-verification rule(c) B believes that A said Na(B thinks I said it)(d) Use of public keys is different than expected. Q encrypting a statement for P does not indicatethe source is Q. Thus, I can forward messages from A and B implying that they are from I.This results in a number of the initial beliefs being incorrect, so the resulting reasoning is alsoincorrect. For example, A believes that it shares Nbonly with B, but it provides it for I as


View Full Document

PSU CSE 543 - BAN Logic

Documents in this Course
Agenda

Agenda

14 pages

HYDRA

HYDRA

11 pages

PRIMA

PRIMA

15 pages

CLIMATE

CLIMATE

15 pages

Load more
Download BAN Logic
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view BAN Logic and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view BAN Logic 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?