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!
