A formalism for visual security protocol modeling

Existing visual modeling paradigms do not adequately cover the visual modeling of security protocols: sequences of interactions between principals in a security system. A visual formalism for security protocol modeling should not only be well-defined but also satisfy certain pragmatic criteria: support for compositional, comprehensive, laconic, and lucid models. Candidate techniques from the OMG's Model Driven Architecture, based largely on UML 2.0, lack a formal syntax and semantics. Well-defined visual formalisms outside of UML have shortcomings with respect to one or more of the pragmatic criteria. We present the GSPML visual formalism as a solution that satisfies all of the pragmatic criteria. We show that GSPML is well-defined with structural operational semantics and a hypergraph grammar syntax.