A Formal Analysis of the Secure Sockets Layer Protocol

Date: 22 October 1997.
Presenter: Sven Dietrich, NASA GSFC/Hughes STX (now Raytheon ITSS).

We present an overview of formal methods for the specification and analysis of authentication protocols and a formal specification and analysis of the Secure Sockets Layers Protocol v3.0. The protocol is specified using an extension of the Rubin-Honeyman NCP logic, based on knowledge and belief, developed for nonmonotonic cryptographic protocols. The existing logic is extended to fit the purpose and the analysis is performed for three specific cases. We draw conclusions about the assumptions of the protocol in general, show the weak points of the protocol, and outline possible attack techniques.

Back to my home page
Last modified: 17 March 1999