Transport Level Security: a proof using the Gong-Needham-Yahalom Logic
arXiv:cs/9904005
Abstract
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.
22 pages, 2 figures, 1 appendix