Transport Level Security: a proof using the Gong-Needham-Yahalom Logic

TL;DR

This paper demonstrates the use of Gong-Needham-Yahalom logic to formally verify the security of the Transport Layer Security protocol, illustrating the method's effectiveness in protocol analysis and education.

Contribution

It provides a formal proof of the TLS protocol using Gong-Needham-Yahalom logic, highlighting its utility in protocol design and verification.

Findings

Formal verification of TLS protocol achieved

Highlights the importance of formal methods in protocol security

Educational value in illustrating protocol authentication subtleties

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.