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.
Cite
@article{arxiv.cs/9904005,
title = {Transport Level Security: a proof using the Gong-Needham-Yahalom Logic},
author = {Walter Eaves},
journal= {arXiv preprint arXiv:cs/9904005},
year = {2007}
}