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


My personal summary is that at least for me it was not possible to find any bugs in this protocol. Furthermore I think that it would be very difficult for anybody to use Murphi to model the whole protocol. After reading the draft several times very carefully I understand how the protocol works. I guess that there are still some bugs in it, but they'll probably appear only in situations that are too specific for Murphi to model. One of the few changes in the draft just released addresses such a bug that was found recently. The following is the short description:

An attack discovered by Daniel Bleichenbacher can be used to attack
a TLS server which is using PKCS#1 encoded RSA. The attack takes
advantage of the fact that by failing in different ways, a TLS server
can be coerced into revealing whether a particular message, when
decrypted, is properly PKCS#1 formatted or not.
For me it seems like a long way to go until such bugs can be discovered with the help of an automatic prover. Nevertheless I think that modeling the TLS protocol was a very good way to understand how this protocol actually works! And I believe that it is reasonable to use a program like Murphi at least for the design of a new protocol.

Tim Wellhausen