[216] in Kerberos
BURROWS SEMINAR
daemon@TELECOM.MIT.EDU (Gail-Lenora Staton)
Wed Sep 23 18:27:32 1987
Resent-From: STATON@XX.LCS.MIT.EDU
From: Gail-Lenora Staton <STATON@XX.LCS.MIT.EDU>
To: saltzer@MULTICS.MIT.EDU
Cc: staton@XX.LCS.MIT.EDU, sollins@XX.LCS.MIT.EDU
Resent-To: kerberos@XX.LCS.MIT.EDU
From: Jerome H. Saltzer <Saltzer@XX.LCS.MIT.EDU>
----- Begin Forwarded Message -----
SEMINAR
DATE: Tuesday, September 29, 1987
TIME: 3:30 p.m. (Refreshments)
TIME: 3:45 p.m. (Lecture)
PLACE: 545 Tech Sq., Room NE43-512A
A LOGIC OF AUTHENTICATION
MIKE BURROWS
Cambridge University
Abstract
We have developed a logic which allows one to describe authentication protocols
and to prove their correctness. It is useful for the designers and implementors
of authentication protocols because:
- it can determine the exact end state of the protocol in terms of the
beliefs of the two authenticated parties;
- it shows up redundant information and redundant encryption in the
protocol;
- it highlights any undesirable assumptions that the protocol relies
upon in order to reach a desired end state;
- it uses concepts which can be understood (were developed!) by people
with little experience with formal techniques.
We have built a theorem checker for the logic, and analyzed various published
protocols, the results of which will be presented.
This work was done by Roger Needham and Mike Burrows at DEC SRC.
HOST: Karen R. Sollins
-------
