In terms of how people who work with security protocols can reason about it, was not-including a spec either in the Standard Notation for security protocols or a sequence diagram on purpose? I thought these were pretty standard conventions.