On 5 January 2013 19:14, Marc Petit-Huguenin <petithug@xxxxxxx> wrote: [snip] > > Another way to look at it would be to run the following experiment: > > 1. Someone design a new protocol, something simple but not obvious, and write > in a formal language and keep it secret. > Which raises the obvious question: Why do we not write protocol specs in a formal specification language instead of struggling with the ambiguities of natural language? Theorem provers and automated verification tools could then be brought to bear on both specifiations and implementations. Dick --