Enhanced security protocol engineering through a unified multidimensional framework

Multidimensional security protocol engineering is effective for creating cryptographic protocols since it encompasses a variety of design, analysis, and deployment techniques, thereby providing a higher level of confidence than individual approaches offer. SPEAR II, the Security Protocol Engineering and Analysis Resource II, is a protocol engineering tool built on the foundation of previous experience garnered during the SPEAR I project in 1997. The goal of the SPEAR II tool is to facilitate cryptographic protocol engineering and to aid users in distilling the critical issues during an engineering session by presenting them with an appropriate level of detail and guiding them as much as possible during design, analysis and implementation. The SPEAR II tool currently consists of four components that have been integrated into one consistent and unified graphical interface: a protocol specification environment (GYPSIE), a GNY statement construction interface (visual GNY), a Prolog-based GNY analysis engine (GYNGER), and a message rounds calculator. The multidimensional approach realized by SPEAR II is combined with a graphical interface that focuses on making specification of a protocol and its associated conditions for formal analysis as straight forward and painless as possible. Experiments that we have conducted confirm that the analysis engine is able to generate accurate proofs for achievable GNY-based goals, while preliminary usability experiments have indicated that the interface utilized by SPEAR II is both expressive and simple to use for specifying cryptographic protocols and constructing logic statements pertaining to these protocols.