CAPSL Tutorial

A CAPSL specification is made up of three kinds of modules: typespec, protocol, and environment specifications, usually in that order. Typespecs declare cryptographic operators and other functions axiomatically. Environment specifications are optional; they are used to set up particular network scenarios for the benefit of search tools. Some standard typespecs in a prelude file are automatically utilized by the CAPSL translator, so many protocols can be specified with only a protocol module.

This tutorial exhibits the most commonly used practice for protocol specifications. For typespecs, look at the prelude. For environment specifications, it is best to read the text of the final report, or the document on the Agent Model.

Protocol Specification

Here is the simplest example of a protocol specification. Protocol Simple1 has only one message, in which principal A sends its name to itself. As in a strongly typed programming language, variables must be declared and typed. Principals are objects that can occur as the source or destination of a message, as well as in a content field.

   PROTOCOL Simple1;
   VARIABLES
      A: Principal;
   MESSAGES
      A -> A: A;
   END;

Assumptions

Here is a slightly more complex example. The HOLDS declaration states that the process executing on behalf of A has been initialized with the principal B chosen as the responder. Read it as ``A holds B.'' If the HOLDS assumption is omitted, the CAPSL translator will complain that sender of the message does not know the receiver address. It is unnecessary to say HOLDS A: A because, by convention, principals always hold themselves.

   PROTOCOL Simple2;
   VARIABLES
      A, B: Principal;
   ASSUMPTIONS
      HOLDS A: B;
   MESSAGES
      A -> B: A;
   END;

Encryption

Certain types of principals possess long-term keys. PKUser is a subtype of Principal possessing a public key pair. If A is of type PKUser, pk(A) is its public key and sk(A) the corresponding private (secret) key. Thus, A could encrypt its message to B as shown.

The notation {field}key is syntactic sugar for the function call ped(key, field). The function ped is the standard abstract public key encryption and decryption function. (If the key is a symmetric key, the syntactic sugar expands internally into a call on se, the standard abstract symmetric key encryption function, instead.)

   PROTOCOL Simple3;
   VARIABLES
      A, B: PKUser;
   ASSUMPTIONS
      HOLDS A: B;
   MESSAGES
      A -> B: {A}pk(B);
   END;

Fresh Keys

Session keys are usually assumed to be fresh, generated in some way that ensures (up to a cryptographically unlikely coincidence) that each new one has not been used before. To be useful as a key, the new value should be unguessable. Sequence numbers, for example, are fresh but not unguessable. Here is an example of session key generation.

In this example, Skey is a symmetric key type, and the declaration of K has two keywords FRESH and CRYPTO called properties. The CRYPTO property indicates unguessability.

Simple4 is not useful because B does not hold K and cannot decrypt the message to obtain A. In CAPSL, this protocol specification is semantically illegal because it implies that B decrypts the message, and the translator will complain that the message is not ``receivable'' by B. Declaring that B holds K does not work, because, in the first message, A cannot generate K as a fresh value if it is already held by B, and the translator complains accordingly. But there is a way to specify that B does not try to decrypt the message.

   PROTOCOL Simple4;
   VARIABLES
      A, B: Principal;
      K: Skey, FRESH, CRYPTO;
   ASSUMPTIONS
      HOLDS A: B;
   MESSAGES
      A -> B: {A}K;
   END;

The Lowe %-Operator

The author of the protocol can specify that B accepts the encrypted term without attempting to decrypt it, by declaring a variable in which B stores the received value. The different views of the message -- the encrypted form seen by A and the atomic form seen by B -- are separated by the % operator, which was introduced by Lowe in Casper. We can see how the % operator is used in this version of the protocol.

The type Field is the supertype of all types that can be used as message fields, including principals, keys, and terms constructed by encryption and concatenation.

The %-operator has a weaker binding precedence than encryption, so, for example, ({A}K)%F can safely be written as {A}K%F.

   PROTOCOL Simple5;
   VARIABLES
      A, B: Principal;
      K: Skey, FRESH, CRYPTO;
      F: Field;
   ASSUMPTIONS
      HOLDS A: B;
   MESSAGES
      A -> B: ({A}K)%F;
   END;

Address Convention

Suppose we wish to extend Simple5 to a longer protocol in which B replies to A with F.

The reply message is unacceptable to the CAPSL translator because ``sender does not know receiver address.'' The problem here is that since B can't decrypt the message, B has not learned the value of A. By convention, the source address of the message is not considered part of the content, and is not readable by the receiver of the message. Realistically, this seems reasonable because, although the same ``Principal'' type is used in the abstraction in both the address and content portions of the message, implementations distinguish an address specification -- such as an IP address -- from a subject name, which is a text string chosen to be meaningful in the application context. Protocols presented in the literature are inconsistent with regard to this convention.
PROTOCOL Simple6; VARIABLES A, B: Principal; K: Skey, FRESH, CRYPTO; F: Field; ASSUMPTIONS HOLDS A: B; MESSAGES A -> B: {A}K%F; B -> A: F; END;

Goals

In order to analyze the security of a protocol, there must be a statement of its objectives. In CAPSL, there is a GOALS section to express secrecy and authentication claims. In the following simple example protocol, we might imagine that the designer intended for K to be a secret shared only by A and B, and that when B receives it, B can be assured that it was sent by A.

These two goals are stated as SECRET and PRECEDES assertions. A SECRET assertion says that the value of a variable generated by its nominal originator cannot be obtained by the intruder (unless the intruder is acting in one of the legitimate roles of the protocol). A PRECEDES A,B | V₁,V₂,... assertion says that if B reaches its final state, then A must have reached a state that agrees with B on V₁, V₂, ....
In this protocol, K as generated by A is kept secret, but it might not reach B. The message received by B could have been forged by the intruder. Thus, the value of K received by B is not necessarily from A, so the PRECEDES goal would fail.

PROTOCOL Simple7; VARIABLES A, B: Principal; K: Skey, FRESH, CRYPTO; ASSUMPTIONS HOLDS A: B; MESSAGES A -> B: {A,K}pk(B); GOALS SECRET K; PRECEDES A: B | K; END;

The Needham-Schroeder Public Key Handshake

This tutorial concludes with the CAPSL specification of the Needham-Schroeder public key handshake. There is a type Nonce used in this protocol which is assumed implicitly, by convention, to have the property FRESH (but not necessarily CRYPTO).


   PROTOCOL NSPK;
   VARIABLES
      A, B: PKUser;
      Na, Nb: Nonce, CRYPTO;
   ASSUMPTIONS
      HOLDS A: B;
   MESSAGES
      A -> B: {A,Na}pk(B);
      B -> A: {Na,Nb}pk(A);
      A -> B: {Nb}pk(B);
   GOALS
      SECRET Na;
      SECRET Nb;
      PRECEDES A: B | Na;
      PRECEDES B: A | Nb;
   END;