Up: Analyzing the TLS protocol
Previous: The TLS protocol
My model of this protocol is based on the work of Ulrich Stern's Murphi model of
the Kerberos protocol. I used the basic structures and the same notation he used
in his work.
The model implements the behavior both of the client and server while trying
to connect. Furthermore there exists an intruder which has the capability of overhearing
and manipulating all messages in the network.
The protocol allows the use of different methods for the key exchange.
The standard methods include the use of RSA or Diffie-Hellman. I implemented only
the key exchange with RSA.
It is assumed that the cryptographic algorithms used by the protocol are safe.
Furthermore it is assumed that it is not possible to attack a certificate.