SAL Tutorial:
The Needham-Schroeder Protocol in SAL

John Rushby

CSL Technical Note


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


BibTeX Entry


Having trouble reading our papers?
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page