SPEAR: a Security Protocol Engineering & Analysis Resource

J.P. Bekmann, P. de Goede and A.C.M. Hutchison
Data Network Architectures Laboratory,
Department of Computer Science,
University of Cape Town,
Rondebosch 7701,
South Africa
E-mail {hutch@cs.uct.ac.za}


SPEAR, the Security Protocol Engineering and Analysis Resource, is a protocol engineering tool which focuses on security protocols, with the specific aims of secure and efficient design outcomes and support for the `production' process. SPEAR offers developers of cryptographic protocols an environment in which to design, analyze and generate security protocols. SPEAR supports protocol specification via a graphical user interface in the style of message sequence charts (MSCs). Security analysis based on cryptographic logics (currently BAN) is facilitated. Production code (currently Java) can be generated once a design has been analyzed. Meta-execution of code allows performance evaluation of cryptographic protocols from within the controlled environment of SPEAR. This paper documents the rationale for, and integration of, these various factors.


The use of open, unreliable networks is increasing as more companies become connected to internetworks. Communications security of these systems is critical and while cryptographic algorithms exist, their security alone is not sufficient to ensure the integrity of a whole system.

One of the most important elements of a cryptographic system is the distributed nature of communicating parties. Since virtually all communication is done via insecure channels, exchange of information can be augmented by cryptographic techniques to provide security via cryptographic (or security) protocols.

It is widely recognized that the engineering of cryptographic protocols is a very subtle task which can easily be deceptive to developers. SPEAR, the Security Protocol Engineering and Analysis Resource, is a protocol engineering tool which focuses on security protocols, with the specific aims of secure and efficient design outcomes and support for the `production' process. SPEAR attempts to marry protocol engineering and formal logical analysis in a tool which greatly simplifies the design, analysis and generation of security protocols.

Security Protocol Engineering and Analysis

Burrows, Adabi and Needham recognize that it is very difficult to design security protocols that achieve their intended function and degree of security [4]. As a result formal methods have been developed to aid in the design and analysis of authentication and other security protocols. The development of logics to analyze security protocols provides one technique for ensuring the correctness of protocols [1]. Logic systems have been used to detect flaws in protocols previously accepted as correct [4,10].

By combining aspects of a formal protocol specification and cryptographic logics SPEAR allows a user to design a security protocol in such a way that there is enough specification for the automatic generation of code that implements the protocol. By integrating aspects of cryptographic logics into this process, logical analysis is naturally incorporated into this design process. The combined expressiveness of this type of specification provides users with a tool which automates the most laborious aspects of the design process and offers a powerful and flexible test-bed for security protocol design.

There are languages available that allow the formal specification of protocols and tools which have been developed in the research of cryptographic logics (e.g. NRL analyzer [18], the Interrogator [16], HOL based Cryptographic logic tool [3]). To our knowledge, however, there are no tools that allow for the easy specification of cryptographic protocols combining both the logics and the formal protocol specifications in such a way as to distil the critical issues and present the user with a higher level design overview. Our tool aims to give users the freedom to explore the critical concepts of security in a controlled and expressive environment without having to actually do an implementation or make use of multiple tools to analyze different facets of a protocol.

Selection of Formalism

In selecting a formalism for representing the specification of a security protocol we primarily contemplated the use of the Specification and Description Language (SDL) [6,2,8]. SDL is in widespread use and has been used extensively in other projects undertaken by our research group, so this was an obvious consideration for us.

SDL is a specification language used to describe communicating systems such as telecommunication protocols. It is an International Telecommunication Uniongif standard, and as such is widely recognized and supported. Recently the textual version of SDL (SDL/PR) has also been augmented with a graphical means of specification (SDL/GR). In this regard SDL is superior to other formal description techniques such as Estelle [14,7] and LOTOS [12] which have only textual representations. There are existing tools such as editors, correctness analyzers, simulators and code-generators for specifications given in SDL. Other members of our group have developed a system called SPECS II (the SDL Performance Evaluation of Concurrent Systems [5,11]) which takes SDL input and performs correctness and performance analysis of protocol input. SPECS II also performs code generation from an SDL specification, and in this respect is similar to other proprietary SDL tools such as Geode [19].

After much deliberation and debate we decided against using SDL as our input formalism. Our reason for not selecting SDL as our specification formalism was largely that SDL does not allow a high-level cryptographic specification, but rather provides a low-level functional specification. While recognizing that it is at the functional level that subtle flaws can be identified, we perceive a lot of common low level functionality amongst cryptographic protocols. By this we mean that although message recipients and contents vary greatly in security protocols, much of the implementational detail such as connections, time-outs, etc. can be seen as common to many actual protocol realizations. Accepting this, one can view SPEAR as being, in fact, at a level above SDL -- where designers can concentrate chiefly on logical security protocol design and actual message contents. In this way they can take advantage of analysis techniques at these levels while still having the possibility to generate SDL as an output of the modelling tool for further analysis should this be desired.

So we have not discarded SDL outright; what we are suggesting is that a full functional specification as required by SDL for each new protocol was not considered the level at which a tool like SPEAR should operate. With a view to allowing prototyping and experimentation, it was instead decided to use a protocol specification technique close to that of Message Sequence Charts (MSCs) [15]. MSCs capture the exchange of protocol messages at a higher level which we believe is more appropriate to cryptographic protocol design, where a lot of effort (and support) is required for message content construction. In SPEAR we have augmented the MSC-like specification with several features which make protocol specification clearer and more intuitive.

Since analysis of message exchanges is also valuable SPEAR can augment a user's protocol description with commonly used elements (of communication, reliability, etc.) to produce a complete SDL output for further analysis by such tools as SPECS II or Geode, if this is required.

Scope of the Tool

Practical experience with developing and deploying cryptographic protocols was the catalyst for developing SPEAR. The time taken to design and implement protocols, and particularly to analyze and tune their implementation, suggested the need for a tool which could encompass all of these aspects. In particular, experience with logic analysis revealed this to be a laborious task when attempted manually. Formulation of a protocol in SDL was again a time-consuming exercise that was not necessarily warranted in terms of, for example, checking for unreachable states or freedom from deadlock.

In this section and those which follow, SPEAR is described at conceptual and architectural levels, and then at the level of realization. At the conceptual level an overview of modules is first given after which each conceptual model is described in turn.

Conceptual Overview

Figure 1 positions SPEAR against the four aspects of security protocol design which it encompasses. Formal protocol specification, security analysis, code generation and meta-execution constitute four distinct, but interconnected modules in SPEAR.

Figure 1:  SPEAR Conceptual Overview

The depiction of SPECS II on the left hand side of the figure locates the security work in our research environment against other protocol analysis work and denotes the possibility to conduct SDL simulation and correctness analysis on the basis of existing available resources.

Protocol Specification

The choice of formalism for protocol specification has been discussed, and Figure 1 reflects that MSCs are the primary formalism with the adoption of some SDL-like features. Figure 2 presents the elements of protocol specification in SPEAR.

Figure 2:  Protocol Specification

The steps necessary to specify a protocol are as follows:

  1. Define the entities (communicating parties) involved in the protocol.
  2. Define the possessions (data items) that are used in the protocol.
  3. Define the external functions that provide a means of assigning initial values to possessions and allow interaction between user, and SPEAR generated, Java source code.

Secondary to these required steps one can:

Following these steps one can perform meta-execution, BAN analysis and performance analysis on the protocol. In Figure 2 GNY analysis and SPECS II are shown as dotted rectangles to indicate future links.

Security Analysis

In terms of security analysis, SPEAR draws on modal logic -- presently BAN -- to reason about the initial, intermediate and final belief and possession sets of principals.

The security of a protocol refers to the secureness of the actual message interchange, the applicability of the respective cryptographic methods, the type and quantity of data sent across insecure channels and the possible attacks that the protocol may be susceptible to. The security analysis module encompasses these aspects and provides automation support. SPEAR provides an automatic means of checking many of the security aspects of a protocol, for example using the previously mentioned logics. The main aim of this is to provide an increased degree of confidence in the protocol and the knowledge that certain types of attacks are not possible, and certain flaws are not exhibited.

Code Generation

Generation of fully functional, portable source code which can be used as actual client and server software is another goal of the SPEAR tool. This removes the networking programming and most, if not all, of the protocol coding. The output is in the form of Java source code classes which can be incorporated into applications that make use of the designed protocol.

Meta-Execution and Performance Evaluation

The SPEAR tool makes a test-bed available to the designer where errors can be detected without having to comprise the security of a real system. One of the features here is execution of the code generated by the code-generation module. This code is augmented with hooks to the SPEAR tool, in such a way that execution can be done in a controlled environment and monitored for performance evaluation.

A longer term aim is also to simulate attacks at a meta-execution level to determine whether protocols are susceptible to certain types of attack (e.g. parallel session or replay attacks).

Architectural Overview

In this section a more detailed overview of the architecture of SPEAR is presented.

Figure 3:  Architectural Overview

Messages are entered in the GUI via textual fields to form a protocol specification.

As these messages are entered they are passed to the Crypto-Expression Parser / Compiler via the Token Handler. They are parsed by the Crypto-Expression Parser and compiled into a token format. Any syntactic or semantic errors are highlighted at this stage.

Token Format

The token format consists of a number of classes which are used to represent a parse tree. For example there is a set class, a function call class, and an identifier class. These classes act as `containers' such that after linking their instantiations (forming ` chains') will combine to form a parse tree.

For example:

RSA:Ka_public( nonce_a, MD5(msg), Kab ) (denoting the encryption of a nonce, a, an MD5 hashed message and a session key, Kab, with a public RSA key called Ka_public) is represented internally in SPEAR as:

new FunctionCall( ``RSA", ``Ka_public", new Set( new Id(``nonce_a"),

new FunctionCall(``MD5",null, new Id(``msg")), new Id(``Kab") ) )

Note that here ``RSA", ``Ka_public", ``nonce_a", ``MD5" and ``msg" would have been defined in the Name Space earlier.

Token Handler Interactions

The Token Handler (nicknamed ``Hairy") acts as the interface to all semantic action of SPEAR. Thus the GUI accesses the Crypto-Expression Parser, Code Generator, logic analyzer (`Crypto Logics'), Meta-Execution and Name Space modules via the Token Handler. The Token Handler module receives declarations of identifiers and functions which it forwards to the Crypto-Expression Parser that verifies names in the expressions with the Name Space module. The Name Space module contains defined identifiers and functions (these are specified via the GUI). The Token Handler also receives tokens from the GUI (which were generated by the Crypto-Expression Parser) and placed within the context of specific protocol entities and message sequences.

The Code Generator Module

Using the defined properties of items (such as entities, data types, full function references etc.) in the Name Space and message sequences, the Code Generator is able to generate the code necessary for message composition and transactions (sending and receiving). This output is currently Java source code, but in future versions will also generate SDL/PR and optionally C++. This is the ``production code".

In order to use this ``production code" in an application, the user would access the functionality of this code via the SPEAR code API which provides the cement for a clean interface and runtime support for the generated code. In order to do performance analysis, code is generated which contains hooks to the GUI for visual presentation of execution information (e.g. rounds and bounds [9]). This is the ``meta-execution" code. The ``meta-execution" code is executed within the context of the meta-execution runtime environment which provides the framework in a similar way as the user environment for the ``production code".

The Crypto Logic Module

The Token Handler calls the Crypto Logics module and supplies the relevant entity definitions and message sequences (defined using the aforementioned token chains). These token chains are translated into a context usable for cryptographic logics such as BAN or GNY. In this release of SPEAR, BAN is implemented, but GNY is planned as a future extension. For the inclusion of GNY a more elaborate translation module is required since GNY has additional rules which are also more complex than those for BAN. The BAN analyzer uses the rules of the BAN logic to derive properties such as possessions and beliefs in the protocol. This information is fed back to the GUI in textual form for presentation to the user.

Protocol Specification Using SPEAR

In this section we show how protocol specification is conducted when using SPEAR.

Figure 4:  Enhanced Needham--Schroeder Protocol on SPEAR

Figure 4 shows the SPEAR tool and reveals its major components by depicting a version of the Enhanced Needham-Schroeder protocol, as it would be defined in SPEAR.

The toolbar on the left hand side of the interface shows the protocol elements that can be added to the protocol canvas -- the central section.

These elements include:

By clicking on the axis (black vertical line) of an entity, protocol elements can be placed on them. In the case of messages, a line is extended from the sender to the mouse pointer which, after clicking on the axis of another entity, results in a line being placed to that entity as receiver. Currently messages can only be sent to single receivers, but support for multiple receivers (as envisaged in, for example, [13]) is a future goal.

The menubar consists of File, Protocol, Options and Help menus. The File menu is concerned with standard file operations while the Protocol menu contains options to modify the protocol as a whole. This includes setting the protocol name, declaring the possessions available to the entities participating in the protocol, declaring the functions that are called to initialize these possessions and general layout functions. The Options menu has elements to configure SPEAR. The Help menu contains help and information regarding SPEAR. The toolbar on the top provides easy access to menu options.

The empty area on the right of the protocol canvas contains information windows which give information about the BAN analysis of the protocol, current status of the meta-execution of the protocol and performance related information. It is predominantly used to convey transient information about the protocol or current status of the protocol to the user.

Declaring Possessions

Before sending messages one needs to declare the possessions that are used in the protocol, and the user functions which will be called. Possessions are then initialized at an entity level -- with each entity using the defined function calls to provide the possessions with initial values. The values of possessions within an entity can also be initialized by receiving messages. For instance a server entity could send the address (IDa) of an authentication entity to a client. The possession IDa would then be defined for the client after receiving the message. Thus although the possessions are declared at protocol level, they are given values at an entity level. In addition the function calls are defined at a protocol level but need not be called (or even defined in every entity).

Figure 5:  Possession Declaration Dialog Box

The Possession Declaration dialog box (Figure 5) is used to declare all possessions available to entities during the run of the protocol. Since this operation is not specific to any entity using these possessions, the dialog is invoked from the Protocols menu option. Each entity then initializes the possessions that it wishes to use as described.

There are currently six types of possessions:

All sizes of data items are specified in bytes.

Building Expressions

Figure 6:  Message Builder Dialog

The Expression Builder dialog (Figure 6) is used to construct messages that are sent across the network. The currently defined possessions are listed on the left and the defined functions are listed on the right. Double-clicking on the left list will replace the current selection with the data item (possession) selected, while double-clicking on the function list will apply the function to the selected area as the argument to that function. Once the message has been constructed one can check the semantic and syntactic correctness of the message. This will highlight incorrectly used functions, non-existent functions and other errors.


To demonstrate the usefulness of the SPEAR tool, a number of security protocols commonly known and used in industry are being extensively dealt with. In addition to evaluation using protocols such as the Enhanced Needham-Schroeder Protocol [17] (as shown in Figure 4), Kerberos and X.509, we will learn from experience gained through designing our own security protocols.

Another project currently underway in our laboratory is development of micropayment protocols and the intention with that project is that once protocol design begins this work will be done on SPEAR. This will provide us with a valuable case study from which to evaluate the utility of our design tool based on the experience of objective users.


Cryptographic protocols are crucial to the increasing use of computer networks for commercial and private communication. For this reason it is imperative that during their design such protocols are systematically scrutinized and refined using the most appropriate techniques. SPEAR is a design environment which supports protocol specification in such a way that security analysis, code generation and meta-execution of a cryptographic protocol can be conducted. SPEAR is intended to fulfill a useful and important function as an integrator and enabler in the discipline of security protocol design.

The SPEAR prototype can be downloaded from: http://www.cs.uct.ac.za/Research/DNA/SPEAR.


This work has been supported by the University of Cape Town Research Committee, the South African Foundation for Research Development and Telkom South Africa.


R. Safavi-Naini A.M. Mathuria and P.R. Nickolas. On the Automation of GNY Logic. Australian Computer Science Communications, 17(1):370--379, December 1995.

Ferenc Belina and Dieter Hogrefe. The CCITT-Specification and Description Language SDL. In Computer Networks and ISDN Systems 16, pages 311--341. 1988/89.

S.H. Brackin. A HOL extension of GNY for automatically analyzing cryptographic protocols. In Proceedings of Ninth IEEE Computer Security Foundations Workshop, Co. Kerry, Ireland, 1996.

M. Burrows, M. Abadi, and R.M. Needham. A Logic of Authentication. ACM Transactions on Computer Systems, 8(1):18--36, February 1990.

M Butow, M Mestern, C Schapiro, and PS Kritzinger. Performance modelling with the formal specification language SDL. In Proceedings of the FORTE/PSTV'96 Conference on Formal Description Techniques, Kaiserslautern, Germany, 1996.

CCITT. Recommendation Z.100: Specification and Description Language SDL, Blue Book, Vol X.1-X.5. ITU General Secretariat, Geneva, 1988.

M. Diaz, J.P. Ansart, P. Azema, and V. Chari. The Formal Description Technique Estelle. North Holland, 1989.

Ove Faergemand and Anders Olsen. Introduction to SDL-92. In Computer Networks and ISDN Systems 26, pages 1143--1167. 1994.

L. Gong. Lower Bounds on Messages and Rounds for Network Authentication Protocols. Proceedings of the 1st ACM Conference on Computer and Communications Security, Fairfax, Virginia, pages 176--183, November 1993.

L. Gong, R. Needham, and R. Yahalom. Reasoning About Belief in Cryptographic Protocols. Proceedings of the IEEE 1990 Symposium on Security and Privacy, Oakland, California, pages 234--248, May 1990.

C Henning, , C Vermeulen, J Zurcher, N de Villiers, C Schapiro, and PS Kritzinger. SDL performance evaluation of concurrent systems: A CASE tool for the development of communicating concurrent systems. In Proceedings of Teletraffic '96, Durban, South Africa, 1996.

D. Hogrefe. Estelle, LOTOS and SDL. Springer-Verlag, 1989.

A. Hutchison and K. Bauknecht. Cryptographic Key Distribution and Authentication Protocols for Secure Group Communication. In Proceedings of the Twelfth International Information Security Conference (IFIP/SEC '96), Samos, Greece, May 1996.

ISO/IEC ISO9074. Estelle, A formal Description Technique Based on an Extended State Transition Model, 1989.

ITU. ITU-TS Recommendation Z.120: Message Sequence Chart (MSC). ITU-TS, Geneva, 1996.

J.K. Millen, S.C. Clark, and S.B. Freedman. The Interrogator: Protocol Security Analysis. IEEE Transactions on Software Engineering, SE-13(2), 1987.

R.M. Needham and M.D. Schroeder. Authentication Revisited. ACM SIGOPS Operating Systems Review, 21(1):7, 1987.

R. Kremmerer and C. Meadows and J. Millen. Three Systems for Cryptographic Protocol Analysis. Journal of Crytology, 7(2), 1994.

Verilog. GEODE Reference Manual. Verilog, 1995.