Specifying Security Protocols by Sequence Diagrams and Goal Models

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 Needham, developers of the BAN logic. Their approach to security protocol verification consist of formalization of the protocol messages; specification of the initial assumptions and protocol goals, and finally applying logic to find flaws in the formally specified protocol. The whole idea is so cool. They have defined semantics for specifying believes of parties of protocol and their goals.

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.