RE: SOI QUESTIONS: 2.6 Formal proofs of security

["Hallam-Baker, Phillip" <pbaker@verisign.com>]

> Was the Needham-Schroeder flaw discovered by a formal proof? 
> (I got the
> impression it was discovered via machine simulation.) It 
> would be nice if we
> had some kind of magical Turing machine that would read in an 
> RFC and tell
> us if the protocol was secure, but in reality the formal methods are
> imperfect because they rely on too much human input.

I have yet to see a really convincing Formal Method for
proving a protocol is secure. I very much doubt that such
a calculus could exist.

The problem being the definition of 'security'. It is certainly 
possible to generate a calculus that will allow a protocol
to be analysed to determine whether it has a particular given 
property, e.g. deadlock freedom, livelock freedom, 'perfect'
forward secrecy under a certain set of assumptions e.g. we
have a cipher suite with certain properties.

The problem is that all formal methods can do is to determine
that a specification has certain properties and security 
problems are very often caused by failing to understand
the requirements.

I believe that the value from formal methods comes from 
addressing a problem in an appropriate formalism so that the
human brain needs to do less work to interpolate the gap
from requirements to specification.

I think there is a lot that the IETF could do to improve the
quality of the standards it produces. However formal methods
are a very long way down on my list, even though I studied them
for my thesis.


First off, there have been tremendous progress in typography
since the invention of the teletype. Typography is a very 
important tool for formatting information in a manner in which
the human brain can best receive it.

The RFC plaintext format is an amateurish anacronism. Not only
does it make producing RFCs tedious, it makes reading and 
verifying them considerably more error prone.

I for one have no intention of reading someone's formal proof
of a specification in RFC plaintext format.

I know this is IETF heresy but there is a reason that Don Knuth
spent all that time developing TeX.

Marshall Rose has been doing some good stuff with XML, use it.


Secondly before adopting formal methods for proof, adopt 
appropriate formal notations for clarity.

If a standard describes a statefull protocol there should be 
a description of the state machine. Preferably this would
be in a notation such as CSP which is formally grounded.


Finally, adopt a mechanism for clearly labelling the 
individual requirements in a requirements document and the 
individual components of an architectural specification.
That will expose the correspondence between the specification
and the requirements. So requirements that are not addressed
become obvious, as do architectural features that do not
address a requirement.

		Phill