The Prelude

This appendix specifies the predefined types. Updated 2/21/01. For readability, this version assumes type inference of undeclared variables, and local scope for variables, neither of which may be implemented.

Basic and Boolean

These types are for basic objects that are not message fields. Note that there is an undeclared "Object" type. No axioms are given for booleans because it is assumed that any protocol analysis tool will have these built in.

TYPESPEC BASIC;
TYPES 
    Role, Spec, Agent: Object;
    Tspec, Pspec, Espec: Spec;
END;

TYPESPEC BOOLEAN;
IMPORTS BASIC;
TYPES
    Boolean: Object;
CONSTANTS
    true, false: Boolean;
FUNCTIONS
    and(Boolean, Boolean): Boolean, ASSOC, COMM;
    or(Boolean, Boolean): Boolean, ASSOC, COMM;
    not(Boolean): Boolean;
    if(Boolean, Boolean, Boolean): Boolean;
END;

Field

The Field type is the universal supertype for all message fields. There is a subtype Atom of Field for fields that can be detached from the left of a concatenation. A type declaration with no explicit supertype implies a supertype of Atom. A Tape is a nonatomic field; it is a concatenated sequence of atoms. The ASSOC property of cat declares that it is associative without the need for explicit axioms.

TYPESPEC FIELD;
IMPORTS BOOLEAN;
TYPES 
    Field: Object;
    Tape, Atom: Field;
    Uid, Nonce, Nat: Atom;
    Principal: Uid, EXPOSED;
FUNCTIONS 
    cat(Field, Field): Tape, ASSOC;
    first(Tape): Atom;
    rest(Tape): Field;
VARIABLES
    X: Atom; 
    Y: Field;
AXIOMS
    first(cat(X, Y)) = X;
    rest(cat(X, Y)) = Y;
    INVERT cat(X, Y): X;
    INVERT cat(X, Y): Y | X;
END;

Symmetric-Key Encryption

The basic Skey type is used by several sets of encryption operators. The only operators given in this root typespec are a hash function and a keyed hash (message authentication code). The DES system could be modeled with the se, sd pair. The only form of single-operator symmetric system that is commonly seen in practice is xor, given below.

TYPESPEC SKEY;
IMPORTS FIELD;
TYPES Skey;
FUNCTIONS
    sha(Field): Skey;
    mac(Skey,Field): Skey;
END;


TYPESPEC DSKE;
IMPORTS SKEY;
FUNCTIONS
    se(Skey, Atom): Atom;
    sd(Skey, Atom): Atom;
    se(Skey, Field): Field;
    sd(Skey, Field): Field;
AXIOMS 
    sd(K, se(K, D)) = D;
    se(K, sd(K, D)) = D;
    INVERT se(K, D): D | K;
    INVERT sd(K, D): D | K;
END;


TYPESPEC XOR;
IMPORTS SKEY;
FUNCTIONS
    xor(Skey, Skey): Skey, ASSOC, COMM;
AXIOMS
    xor(xor(K,K),K1) = K1;
    INVERT xor(K,K1): K | K1;
    INVERT xor(K,K1): K1 | K;
END;


/* Symmetric Key Client, Server */

TYPESPEC SKCS;
IMPORTS SKEY;
TYPES Client, Server: Principal;
VARIABLES
	S : Server;
	C : Client;
FUNCTIONS
	 csk(Client): Skey, PRIVATE;
	 ssk(Server,Client): Skey, PRIVATE; 
AXIOMS
	 ssk(S, C) = csk(C);
END;


/* Mutual Symmetric Key Node */

TYPESPEC MSKN;
IMPORTS SKEY;
TYPES Node: Principal;
FUNCTIONS
	msk(Node, Node): Skey, COMM, PRIVATE;
END;

/* Arithmetic operations may be used in CAPSL with the
infix syntax +, -, *, /, ^.
*/

TYPESPEC ARITH;
IMPORTS SKEY;
CONSTANTS 1: Skey;
FUNCTIONS
    pls(Skey, Skey): Skey, ASSOC, COMM;
    mns(Skey): Skey;
    tms(Skey, Skey): Skey, ASSOC, COMM;
    div(Skey, Skey): Skey;
    exp(Skey, Skey): Skey;
/*
AXIOMS
*/
END;

Public-Key Encryption

As in symmetric-key encryption, there is a basic public-key type, used for both public and private keys. The single-operator version ped models RSA at a very abstract level.

TYPESPEC PKEY;
IMPORTS FIELD;
TYPES Pkey;
FUNCTIONS
    keypair(Pkey, Pkey): Boolean, COMM;
END;


TYPESPEC SPKE;
IMPORTS PKEY;
FUNCTIONS
    ped(Pkey, Atom): Atom;
    ped(Pkey, Field): Field;
AXIOMS 
    if keypair(K, K1) THEN ped(K1, ped(K, X)) = X ENDIF;
    if keypair(K, K1) THEN INVERT ped(K, X): X | K1 ENDIF;
END;

/* PPK provides simple standard public/private key lookup. */

TYPESPEC PPK;
IMPORTS PKEY;
TYPES PKUser: Principal;
FUNCTIONS
  sk(PKUser): Pkey, PRIVATE;
  pk(PKUser): Pkey;
AXIOMS
  keypair(sk(P),pk(P));
  INVERT ped(sk(P),X): X | pk(P);
  INVERT ped(pk(P),X): X | sk(P);
END;

Key Agreement

This key agreement type is meant to express the basic properties of Diffie-Hellman key agreement. The kap operation creates a public value that can be combined with an Skey to produce another Skey using kas. This type specification omits significant relations that emerge when kap is implemented by raising a known base value to the Skey power modulo a prime.

TYPESPEC KeyAgreement;
IMPORTS SKEY;
TYPES Pval;
FUNCTIONS
    kap(Skey): Pval;
    kas(Pval, Skey): Skey;
AXIOMS
    kas(kap(Ka),Kb) = kas(kap(Kb),Ka);
END;

Public-Key Sealing

The following public-key seal operation could be implemented with a keyed hash, but it may also be viewed as a primitive operation. It could be the basis for a signature if one assumes that the sealing key is private to the signer.

TYPESPEC PKSeal;
IMPORTS PKEY;
TYPES Pseal;
FUNCTIONS
    seal(Pkey, Field): Pseal;
    verify(Pkey, Pseal, Field): Boolean;
AXIOMS
    IF keypair(K, K1) THEN verify(K1,seal(K, X), X) ENDIF;
END;

Timestamps

Timestamps are used simply by assuming that each agent that generates or checks a timestamp holds it initially. Equality comparisons can be used to simulate "nearness." A more advanced version might check ordering.

TYPESPEC TIMESTAMP;
TYPES Timestamp, EXPOSED;
END;

List

TYPESPEC LIST;
IMPORTS FIELD;
TYPES List;
FUNCTIONS
    con(Field, Field): List;
    head(List): Field;
    tail(List): Field;
AXIOMS
    head(con(X, Y)) = X;
    tail(con(X, Y)) = Y;
    INVERT con(X, Y): X;
    INVERT con(X, Y): Y;
END;

End Prelude Marker

This type is placed at the end of the prelude to mark the separation of symbols and axioms in the prelude from those in user-supplied typespecs. This separation is helpful for connectors that provide built-in support for the prelude types.

TYPESPEC ENDPRELUDE;
CONSTANTS endprelude: Boolean;
AXIOMS
    endprelude = true;
END;