SVO

SVO has 22 rules and 13 language concepts. SVO is intended to be more formal than BAN and simpler than GNY . SVO is different from BAN in few important ways. SVO is message based, so there are no type flaws (i.e a person knows if he is recieving a message, key, etc.). SVO allows negation and assumes principals are competent (generated R.V.'s (nonces) are good). It has distinct public key types for encryption, signatures, and key exchange. SVO includes the rationality rule, Being Told, Possession and many of the recognizability and freshness rules of GNY but stears clear of R6 . And most importantly for the problems presented above it has the concept of a principal representing the environment, i.e. an eavesdropper.

Let us look at how cleverly SVO is able to avoid falling into Nessets pit. SVO assumptions of the protocal are:

• A believes A controls keys between A,B.
• A believes .
• B believes A controls keys between A, B.
• B believes .
• B believes

So the analysis goes:

• Step 1: B sees
  • By rule 4: B believes A said .
  • By rule 15: B believes a key for A,B.
• A sees By rule 4: A believes B said .

conclusion: A,B believe is a good key for A and B.

This doesn't look good, but note that we did not take into consideration in our analyses the principal representing the enviroment. For the eavesdropper E we need to add the initial assumption:

• E believes

and we can infer in Step 1:

• By rule 7: E received .

Hence is not a good key for A and B.

Let us now look at the difference of these three logics by looking at what they conclude from Kerberos :

• GNY
  • A, B both believe is a key for them. (i.e. will believe anything encrypted in the key came from the other person).
  • A believes B possesses .
• SVO
  • A, B both believe is a key for them.
• BAN
  • A, B both believe is a key for them.
  • A believes B believes is a key for A,B.
  • B believes A believes is a key for A,B.

And what they conclude from Needham-Schroeder Public Key.

• GNY
  • A believes .
  • B believes .
• SVO
  • A, E believe
  • B, E believe
• BAN
  • A believes is B's key.
  • B believes is A's key.
  • A believes B believes is a secret key for A,B.
  • B believes A believes is a secret key for A,B.

So basically BAN allows us to conclude more than GNY, which allows us to conclude more than SVO.BAN has 19 rules and 10 language concepts, while GNY has 45 and 13 and SVO 22 and 13 so Summary of differences:

• GNY
  • A rule R6: if A has seen H(X), A can recognize X.
  • X says Y doesn't mean X believes Y.
  • Concept of Not-originated-here and recognizability.
  • Considers plaintext.
• SVO
  • Has an "environment" (or attacker).
  • Assumes competency.
  • Well-typed (Messages based).
  • Considers plaintext.

Conclusions:

On the upside we have that logics provide a framework for structured analysis. Logics can be useful for finding flaws. BAN for instance found a flaw in X509 and other protocols. On the downside we have that logics don't find all flaws. Logics are very cumbersome to apply by hand. Picking assumptions is almost as ad hoc as designing the protocol. Semantics are hard to nail down (what is authentication?). Logics are limited in what they can represent ( in BAN for instance saying is same as believing). A logic designed to analyze a protocol can be as difficult to prove correct as the protocol itself, if not more so.