SAL Tutorial:
The Needham-Schroeder Protocol in SAL
John Rushby
CSL Technical Note
Abstract
The Needham-Schroeder authentication protocol is specified in SAL and
its model checker is used to detect the flaw discovered by Gavin Lowe.
The SAL simulator is used to further explore the model of the protocol.
This provides a simple illustration in the use of SAL for this domain.
gzipped postscript,
or
plain postscript
or
PDF
or
crude ascii (for your Palm Pilot)
SAL Files
network.sal
needhamschroeder.sal
BibTeX Entry
TBD
Having trouble reading our papers?
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page