J.P. Bekmann, P. de Goede and A.C.M. Hutchison
Data Network Architectures Laboratory,
Department of Computer Science,
University of Cape Town,
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.
Burrows, Adabi and Needham recognize that it is very difficult to design security protocols that achieve their intended function and degree of security . 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 . 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 , the Interrogator , HOL based Cryptographic logic tool ). 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.
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 Union 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  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 .
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) . 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.
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.
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.
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:
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.
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.
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.
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).
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.
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.
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.
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.
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 ). 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 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.
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, ) 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.
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.
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  (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.