[langsec-discuss] Is computation half the story?

Scott Guthery sbg at acw.com
Fri Mar 27 13:10:35 UTC 2015


>>> By "theory" I mean a general system of knowledge and understanding. 
>>> Think "theory of evolution", not "theorems."

But why not think theorems?  A general theory while certainly helpful for 
framing questions can not be the foundation for making security assertions 
about a system at hand any more than the general theory of evolution tells 
us how the eye evolved.    The theorem approach has worked well in the area 
of authentication protocols and has led to the discovery of undesirable 
propertie. The break of the Needham and Schroeder protocol is, perhaps, the 
most well-known example.  Nobody knew the hole was there until Gavin Lowe 
among others tried to prove the a property of the protocol that wasn't 
there.

Formal analysis (the theorem approach) can handle composition of systems and 
cascading of systems in the same manner that today's mathematics is built on 
yesterday's.  Boyer and Moore proved theorems about an entire computational 
stack from chip net list to programming language.

Yes, it's hard work.  But it yields hard results.  General theories are 
necessary for the framework but they can't tell us anything specific such as 
can Attack A succeed against System B.  People running and using 
computational systems need specifics, not generalities.

IMHO, as always.

Cheers, Scott



More information about the langsec-discuss mailing list