[217] in Kerberos
[Gail-Lenora Staton : Burrows Seminar - NEW TIME]
daemon@TELECOM.MIT.EDU (Karen R. Sollins)
Tue Sep 29 12:44:00 1987
Resent-From: SOLLINS@XX.LCS.MIT.EDU
From: Karen R. Sollins <SOLLINS@XX.LCS.MIT.EDU>
To: csr-people@COMET.LCS.MIT.EDU
Resent-To: kerberos@XX.LCS.MIT.EDU
From: Jerome H. Saltzer <Saltzer@XX.LCS.MIT.EDU>
1. Note change in time.
2. Mike Burrows stopped by to talk for a few minutes this morning.
He says that his talk will include an analysis of exactly what you
know for sure when each of several authentication protocols,
including Kerberos, is completed.
Jerry
----- Begin Forwarded Message -----
Date: Tue 29 Sep 87 10:08:08-EDT
From: Gail-Lenora Staton <STATON@XX.LCS.MIT.EDU>
Subject: Burrows Seminar - NEW TIME
To: tech-sq@XX.LCS.MIT.EDU
***TODAY **** TODAY **** TODAY **** TODAY **** TODAY **** TODAY***
SEMINAR
DATE: Tuesday, September 29, 1987
NOTE NEW TIME ====> TIME: 3:00 p.m. (Refreshments)
NOTE NEW TIME ====> TIME: 3:15 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
-------
-------
