next up previous
Next: Results Up: Analyzing the TLS protocol Previous: The TLS protocol

Murphi model of TLS

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.

Tim Wellhausen