next up previous
Next: Conclusion Up: Analyzing the TLS protocol Previous: Murphi model of TLS


After implementing the exchange of all messages between client and server I had to realize that it seems not to be possible to attack this protocol with Murphi as long as certificates are used. If RSA is used, the public key of the server is part of the certificate. Suppose that the certificate cannot be changed by an intruder (this could also be a subject for proving), then the client gets the authenticated public key of the server which it uses to send a pre-master secret. Together with the random values exchanged in the beginning, the master secret is computed. The draft describes in detail how a possible attack with replayed or generated messages will fail because of the exchange of specific messages. For example an encrypted MD5 checksum of all handshake messages is sent in the end. I tried to implement an intruder that is able to store and send messages that he overhears. But because of the large number of messages, this blows up for one client and one server even with the hash table compression and a lot of memory. Finally I decided to reproduce a possible attack that is described in the draft. This attack is only possible if client and server agree on a cipher suite that doesn't demand server authentication. That means there are no certificates involved. Without authentication a man-in-the-middle attack is possible. The intruder has to intercept the ServerKeyExchange witch contains the public RSA key of the server and has to send a new ServerKeyExchange message with his own RSA key to the client. When the client sends the pre-master-secret which is now encrypted with the intruder's key, the intruder has to intercept again and send the pre-master-secret with the server's public key to the server. Together with the random values which the intruder can overhear, it can easily compute the master secret without anybody knowing that there is an intruder. For this the intruder has to keep track of all messages, and to manipulate the MD5 checksum at the end of the handshake. My implementation of this attack consists of an intruder that overhears all important information and generates new KeyExchange messages. I assume that the intruder would be able to send only messages if they would be accepted by the destination. This is possible if the intruder stores information about all messages sent. I skiped this in order to avoid the next blow-up. Furthermore, I didn't model the exchange of the correct checksum in the end. The following is an extract of Murphi's output for this attack:

Startstate Startstate 0 fired.
Rule Client sends ClientHello to server.
Rule intruder overhears/intercepts.
Rule Server receives ClientHello from a client and sends ServerHello.
Rule intruder overhears/intercepts.
Rule Client gets ServerHello message.
Rule Server sends ServerKeyExchange.
Rule intruder overhears/intercepts.
Rule Intruder sends generated ServerKeyExchange message to client.
Rule Client gets ServerKeyExchange message from server.
Rule Server sends ServerHelloDone.
Rule Client gets ServerHelloDone message from server.
Rule Client sends the ClientKeyExchange message.
Rule intruder overhears/intercepts.
Rule Intruder sends generated ClientKeyExchange message to server.
Rule Server gets ClientKeyExchange message.
Rule Client sends the ChangeCipherSpec message.
Rule Server gets ChangeCipherSpec message.
Rule Client sends the Finished message.
Rule Server gets the Finished message and sends ChangeCipherSpec message.
Rule Client gets ChangeCipherSpec message from server.
Rule Server sends Finished.
Rule Client gets Finished message from server.

End of the error trace.


        Invariant "Intruder must not have the master secret
        of a running connection." failed.

State Space Explored:
        1161 states, 2759 rules fired in 0.65s.
I also tried this attack with two clients, two servers and one intruder. It took 246837 states until the same result was computed.
next up previous
Next: Conclusion Up: Analyzing the TLS protocol Previous: Murphi model of TLS
Tim Wellhausen