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);
}

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) ];

  tag MTag (Msg(a,b)) : Auth(a:Host, b:Host);

The type for the shared key is simple:

  private SKey : SharedKey(Alice,Bob);

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