next up previous
Next: About this document Up: No Title Previous: GNY

SVO

SVO has 22 rules and 13 language concepts. SVO is intended to be more formal than BAN and simpler than GNY gif. 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:

So the analysis goes: conclusion: A,B believe tex2html_wrap_inline166 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:

and we can infer in Step 1:

Hence tex2html_wrap_inline166 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 gif:

And what they conclude from Needham-Schroeder Public Key. 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: 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.


next up previous
Next: About this document Up: No Title Previous: GNY

Bjarni V Halldorsson
Fimmtudagur, 23. október 1997 21:19:54