Using GYPSIE, GYNGER and Visual GNY to Analyze Cryptographic Protocols in Spear II
Elton Saul, Andrew C. M. Hutchison · 2001
The development of cryptographic logics to analyze security protocols has provided one technique for ensuring the correctness of these protocols. However, it is commonly acknowledged that analysis using a modal logic such as GNY tends to be inaccessible and obscure for the uninitiated. In this paper we describe the SPEAR II graphically-based security protocol engineering environment that can be used to easily conduct GNY analyses. SPEAR II consists of three primary components: a protocol specification environment (GYPSIE), a GNY statement construction interface (Visual GNY) and a Prolog-based GNY analysis engine (GYNGER). In contrast to other tools, SPEAR II offers a multi-dimensional approach to protocol engineering, integrating protocol design and analysis into one consistent and unified interface. The interface and techniques used within this tool are built on the foundation of previous experience with the original SPEAR tool and GNY analysis research. We also show how the SPEAR II tool is used to conduct a GNY analysis and how it distances protocol engineers from any associated syntactical issues, allowing them to focus more on the associated semantics and distil the critical issues that arise. By freeing individuals to focus on an analysis, instead of hampering them with the necessary syntax, we can ensure that the fundamental concepts and advantages related to GNY analysis are kept in mind and applied as well.