Transport Level Security: a proof using the Gong-Needham-Yahalom Logic
Walter Eaves · arXiv (Cornell University) · 1999
This paper provides a proof of the proposed Internet standard Transport Level Security protocol using the Gong-Needham-Yahalom logic. It is intended as a teaching aid and hopes to show to students: the potency of a formal method for protocol design; some of the subtleties of authenticating parties on a network where all messages can be intercepted; the design of what should be a widely accepted standard.