mjl@cs.rit.edu (12/12/89)
I sometimes believe the following forms a tautology:
let R = {all readers of comp.software-eng}
let SWEOS = {r in R | r believes OS's have something to do with s/w eng.}
let SWEMATH = {r in R | r believes math has something to do with s/w eng.}
SWEOS intersect SWEMATH = {mjl@cs.rit.edu}
Be that as it may, here goes:
I just returned form the 12th ACM Symposium on Operating Systems
Principles. One of the better papers presented was "A Logic of
Authentication" by Burrows, Abadi, and Needham. A capsule summary will
not do full justice to the paper, but basically the authors devised a
set of axioms that captures many of the intuitive notions surrounding
authentication systems like Kerberos. They then used these axioms to
derive formal properties of several such systems. What made the paper
particularly interesting from an engineering viewpoint was that this
formalization revealed both anomalies and redundancies in a variety of
common authentication systems, including the recommended CCITT X.509
authentication protocol. It appears that once a flaw was discovered by
the axioms, it was quite simple to deduce where the flaw actually was
embedded in the protocols. I assert that results like these support
my contention that mathematical approaches to software specification,
analysis, and design are not inimical to good software engineering, but
rather a key element of same.
In any event, I recommend the article to one and all. It will come out
soon in Vol. 23 No. 5 of the SIGOPS Operating Systems Review.
Mike Lutz
mjl@cs.rit.edu
Mike Lutz Rochester Institute of Technology, Rochester NY
UUCP: {rutgers,cornell}!rochester!rit!mjl
INTERNET: mjlics@ultb.isc.rit.edu