Evaluating logics

How do we decide what are good logic? Clearly we need logics to be sound (we can't derive invalids and complete (we can get all we want). Once we have taking care of that we can look at secondary objectives like complication and how formal the logics is.

It was shown by Nesset that BAN logic is not complete. Nesset propossed the following protocol with the obvious flaw that is sent in the clear in step 1 (anyone can intercept the message and pretend to be B). :

1. 
2. 

Idealized:

1. 
2. 

BAN analysis assumptions of the protocol are the following:

1. B believes
2. A believes
3. A believes
4. B believes
5. B believes (A controls

So we can deduce:

• B sees , hence B believes A said , hence B believes A believes , B believes A controls hence B believes .
• A sees . So A believes B said , and thus A believes B believes .

So A and B believe they share a secret key which no-one else has access to, which is clearly not true.

This analysis was though highly critized and one of the strongest criticism came from the inventors of BAN, Burrows, Abadi and Needham, pointed out that assumption 2, A believes is flawed because the key is effectively sent in the clear and said: "This inconsistency is not manifested by our formalism, but is not beyond the wit of man to notice. From this absurd assumption, Nessett derives an equally absurd conclusion, in keeping with the principals of logic."

Other critics have also pointed out that that it is not clear that the correct assumption where picked for the analysis, that BAN is not intended to find all security problems (so even though it is not complete it is of use) and that BAN logics is not really a formal logic since it allows you to invent arbitrary rules.

Let us now look at another example where BAN fails us. Recall Otway-Rees from last hour. BAN's analysis assumptions are:

• A, S believe is a good key for them.
• B, S believe is a good key for them.
• S believes is a good key for A and B.
• A, B believe S has jurisdiction over each other's "once said" and keys between them.
• B believes is fresh.
• A believes and fresh.

So we can conclude:

• A and B believe is a good key for A and B.
• A believes B once said .
• B believes A once said .

But this protocol is subject to misauthentication of a malicious party. Let us look at how Mallory can masquare as Bob to Alice:

• to Bob: .
• Bob to Trent:
• Trent rejects the message because he cannot decode garbage.
• Alice sends to : .
• sends to Trent: . Mallory uses the message Bob sent to Trent.
• The protocol goes through, and Mallory has successfully masqueraded as Bob.

Where is the bug? M was preplayed, hence it wasn't fresh. Clearly Otway-Rees was interested in freshness but used a sequence number instead of a random nonce. If we fix Otway-Rees by picking a random nonce for M, the new proof ought go through, hence the only possible assumption is the freshness of M. So is our assumption that A can believe the freshness of M wrong? Remember the definition of freshness.

"X is fresh if it has not been sent in a message at any time before the current run of the protocol". Well B did once say so that not really a problem. BAN's definition of authentication is not good enough, the exchange key only establishes that they said something. The protocols flaw is an oracle flaw, Bob always replies, BAN doesn't deal with oracle flaws.

We will now present two doxastic logics which try to mend the flaws of BAN:

• GNY (Gong, Needham, Yahalom)
• SVO (Syverson and van Oorschot)

Let's firtst summarize BAN's flaws:

• Simplicity, less power, does not allow temporal notions, negation and some other notions. BAN has 19 rules and 10 language concepts.
• Idealization is a problem:
  • No formal rules to do idealization.
  • There is a gap between the formal protocol and the idealized protocol.
  • It is easy to create flaws during idealization step.
• One can only say what he believes.
• Making initial assumptions is nontrivial and ill-defined.
• Some notations like freshness are ill-defined.