Up: Analyzing the TLS protocol
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.