Andrew D. Gordon
Microsoft Research

Christian Haack
Radboud University

Alan Jeffrey
Bell Labs

Cryptographic Protocol Type Checker

Introduction

Applet

Examples

Download

Research Papers

Changelog

To Do List

Introduction

Overview

The Cryptyc system is a Cryptographic Protocol Type Checker. Unlike most typecheckers, it does not just check for simple data errors, such as dereferencing an integer or treating a pointer as a boolean. It can also statically check for security violations such as secrecy or authenticity errors.

The Cryptyc system is implemented as a Java applet and as a command-line application. You can use the applet to edit sample protocols, and to typecheck the protocols to ensure they do not violate the security policies.

Security policies are determined in two ways:

  • Data is typed as either Public or Private, and only Public data is ever leaked to an attacker.

  • Protocols are instrumented with begin and end markers for authenticity, and the typechecker ensures that any end marker can only be reached if a matching begin marker has previously been reached. Since an end can match a begin provided by a different participant, these correspondence assertions allow simple authenticity properties to be stated and verified.

These policies are enforced by a type checker, which checks that the trust placed in the protocol (in particular its use of keys and nonces) is justified. Any protocol which passes this typechecker is secure against the so-called Dolev Yao attacker (an intruder with the power to intercept and forge messages, but without the power to crack encrypted messages without the key).

This type system has been implemented as an applet, and as a command-line tool, and has been used to analyse authenticity properties of a number of protocols including Needham-Schroeder, Otway-Rees and Woo and Lam.

Insecure example

The Cryptyc tool takes as input a protocol written in a protocol specification language based on a variant of Abadi and Gordon's Spi Calculus, which in turn is based on Milner, Parrow and Walker's Pi Calculus.

The protocol defines a number of participant processes, some of which are clients and some of which are servers. Clients can initiate socket connections to servers, and then communicate data along the socket.

For example, a simple client called Sender running on Alice's machine which makes a socket connection to send a new public message is:

  client Sender at Alice is {
    initiate Receiver at Bob is (socket : Socket);
    new (msg : Public);
    output socket is (msg);
  }

The matching server running on Bob's machine is:

  server Receiver at Bob is (socket : Socket) {
    input socket is (msg : Un);
  } 

The received message has untrusted type Un, because it is read from an untrusted channel. To instrument this protocol with authenticity information, we add begin and end markers to the protocol. For example:

  client Sender at Alice is {
    initiate Receiver at Bob is (socket : Socket);
    new (msg : Public);
    begin! (Alice sending msg to Bob);
    output socket is (msg);
  }

  server Receiver at Bob is (socket : Socket) {
    input socket is (msg : Un);
    end (Alice sending msg to Bob);
  }

In order for a protocol to be safe we require that every executed end marker must be preceded by a matching begin marker. For example the above protocol is safe.

In order for a protocol to be robustly safe we require that it is safe even in the presence of an attacker who can intercept and forge messages. For example the above protocol is not robustly safe, since an attacker can forge messages from Alice, causing Bob to execute end (Alice sending msg to Bob) without Alice having executed begin (Alice sending msg to Bob).

Secure example

To make this protocol robustly safe, we have to introduce cryptographic primitives: encryption and message tagging. We assume that Alice and Bob share a key SKey. Moreover, we assume that MTag is a global message tag. Alice now tags and encrypts her message before sending it. The amended protocol is:

client Sender at Alice is {
  establish Receiver at Bob is (socket : Socket);
  new (msg : Public);
  begin! (Alice sending msg to Bob);
  output socket is { MTag(msg) }SKey;
}

server Receiver at Bob is (socket : Socket) {
  input socket is { MTag(msg : Public) }SKey;
  end (Alice sending msg to Bob);
}
The message tag is used to avoid confusion between different messages encrypted under Alice and Bob's shared key. The tag is not strictly necessary for robust safety of this simple protocol in isolation. However, in a more realistic scenario, Alice and Bob use their same shared key in other protocols in parallel. Our type system can verify the protocol without the message tag, but this would require a protocol-specific type for the shared key.

Type Annotations

This protocol is robustly safe, but we now have to convince the Cryptyc tool of this. We do this by providing types for all of the data involved with the protocol. First, we define a pattern that all messages tagged by MTag are required to match (see pattern matching for details):

  pattern Msg (a:Host, b:Host)
     = ( msg : Public ) [ !begun (a sending msg to b) ];
Note that the defined message pattern depends on parameters a and b of type Host.

Next, we declare the type of MTag:
  tag MTag (Msg(a,b)) : Auth(a:Host, b:Host);
This type expresses the following constraint on the use of MTag: This tag may only be used to tag messages that match pattern Msg(a,b) for some hosts a and b. The resulting tagged message has either type Private(a,b) or type Public(a,b) (depending on whether or not the message has unencrypted private parts). Let's look at the example: At the point where Alice forms MTag(msg), the marker begin! (Alice sending msg to Bob) has been executed. Therefore, msg matches the pattern Msg(Alice,Bob). Thus, MTag's type permits the formation of MTag(msg), which has type Public(Alice,Bob).

The type for the shared key is simple:

  private SKey : SharedKey(Alice,Bob);
The key word private that precedes the type declaration indicates that SKey may not be revealed to possible attackers.

Types of the forms Public(a,b) or Private(a,b) are called authorization types. Messages of these types require authorization by a and b. Authorization can be acquired by encrypting the message with a key of type SharedKey(a,b). In the example, Alice acquires authorization for message MTag(msg) of type Public(Alice,Bob) by encrypting it with Alice and Bob's shared key SKey of type SharedKey(Alice,Bob). Although it would also be legal for Alice to publish the unauthorized message MTag(msg), the receiver Bob would not typecheck if he received an unauthorized message.

Running the tool

We have now verified that the example protocol is robustly safe. The source code is in intro-example.cry, and can be typechecked on the command-line using the cryptyc.jar jar archive:

  java -jar cryptyc.jar intro-example.cry

Alternatively, it can be checked using the applet page.

Credits

The Cryptyc language was designed and formally proven correct by Andrew D. Gordon, Microsoft Research, Christian Haack and Alan Jeffrey, DePaul University. The Cryptyc implementation was developed by Christian Haack and Alan Jeffrey.

Thanks to Martín Abadi, Dusko Pavlovic, Benjamin Pierce, Corin Pitcher, James Riely, and Andre Scedrov for discussions about this work.

Alan Jeffrey was funded in part by Microsoft while writing the research papers which form the basis of the Cryptyc project.

Cryptyc implementation Copyright © 2001-2004, Alan Jeffrey and Christian Haack
Technical reports Copyright © 2000-2004 Microsoft Research, Alan Jeffrey and Christian Haack
This material is partly based upon work supported by the National Science Foundation under Grant No. 0208549.
Last modified: Wed Nov 10 12:25:07 2004