Are formal methods used for cryptographic protocol design?

Question

I decided to learn more about the application of formal methods to cryptographic protocols and found this interesting talk by Cathy Meadows at YouTube.

After doing research about how people are using formal methods, it seems to me that they're not being used for design. In other words, formal methods are being applied by researchers to cryptographic protocols that were already designed and published by organizations.

Why are those organizations not applying those same formal methods while they're designing the protocol? Why don’t those organizations seem to care about formal methods in the first place? Is there a disagreement between academia and industry about the usefulness of those tools?

Answer 1

In my experience the persons doing the standardization may not know about formal methods in the first place. And even if a formal method was used, they would not know how to assess it.

Note that whatever mathematical method is applied, the security of a protocol is still dependent on how the domain was modelled. If the model is even slightly incorrect, a protocol may still be insecure. It would not be the first time - to put it mildly - that a security proof has to be reconsidered.

Answer 2

One of the main reasons why formal methods are not used widely in the design phase is the lack of automation. It is often hard to see how one refines an original design of security protocol to a more concrete model while preserving properties of interest. There has indeed been research on this direction which is called security protocol refinements. However, so far the correctness of refinement steps are often formalized and checked in Higher Order Logic theorem provers and require a certain level of expertise. For non-expert users, a full automation is still out of reach.