Cryptographic protocols, especially ones for authentication purposes, are complicated and hard to understand if you read the sequences of plain or encrypted values that the parties send back and forth. But are they understandable for a machine or tool that verifies the security and vulnerabilities of the protocols? There exists very interesting research on formal verification of security protocols which mainly results of work of three people: Burrow, Abadi and
I am not a security expert, and probably I will have a hard time understanding this approach. However, I have some ideas to improve the understandability of specification of protocols and goals of messages sent and received, by relating the steps of the protocol to goal models. Goal models, which basically I spend most of the time playing with them, capture and express “why” in addition to “how” and “what” aspects. A famous goal- and agent-oriented modeling and analysis framework in this regard is i*. Currently, I am thinking how to express a protocol both in sequence diagrams and i* models to improve the semantic and also understandability of the models.