It’s important to formally specify your protocol. Hence:
You can see it’s formal because I added a gratuitous sigma.
We implemented the protocol in two different tools, written in two different languages and after two minor tweaks, it worked. Thank you formal specification!
Time person of the year 2006, Nobel Peace Prize winner 2012.