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:
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:
Let us now look at the difference of these three logics by looking at what they conclude from Kerberos :
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.