The Agent Model

Updated 4/11/00. There was an February 1999 version of this note, also August 1998 and a Feb. 1998 version also.

Introduction

Protocol specifications in CAPSL, like most textbook protocol specifications, are written from the point of view of a single protocol session. Two or three principals are conversing among themselves according to the given message sequence and formats, and their roles are defined in a context that is oblivious to attacker interference, or the existence of other, concurrent sessions of the same or different protocols.

Models for analyzing attacks generally require a more explicit awareness and representation of the network environment, which includes the attacker and multiple sessions. Other sessions may have been completed in the past, or they may be running concurrently. Each participant in the protocol is a process, called a protocol process or agent, which is characterized both by its role in the protocol and by its owner, the principal on whose behalf or authority it operates.

Each protocol variable of type Principal has a role implicitly associated with it. The CAPSL compiler derives the transition rules for each role, expressing them in an intermediate language (CIL).

A principal is a persistent entity that possesses long-term information such as private keys. Principals may be users (Alice, Bob) or long-lived well-known processes (e.g., a database server or key distribution center).

Principals are grouped into subtypes according to what long-term information they possess. The subtypes depend on the protocol. A protocol using a symmetric key system may, for example, divide principals into clients, each of which has one key shared with any server, and servers, which have an array of keys, one for each client that uses it.

One important point about principals as permanent entities is that they may have many agents acting on their behalf, in the present or in the past. All agents of the same principal share the same long-term keys and other such information. This is relevant for analysis because it means that messages or message fields from one protocol session may be using the same long-term keys as those in another session. Such messages are potentially useful in an attack that involves replaying information from one session into a different session.

Note also that principal may have agents playing different roles in the protocol. An agent of subtype Client can usually act either as an initiator or a responder.

Agents

An agent is a short-term or per-session entity that acts on behalf of some principal and behaves according to one of the roles specified in the protocol. An agent is an object whose state components include (1) its role, associated with the name of a variable of type Principal (or some subtype); (2) its owner, the particular object of type Principal assigned to that variable; (3) a state label, typically an integer whose value changes with every transition, and (4) its holdings, the values associated with protocol variables. In a given state, a protocol variable may be held or not. If held, its value was given initially or acquired during execution. If not held, the value may be regarded as null.

Principal Subtypes in CAPSL

CAPSL has the TYPESPEC syntax to introduce abstract data types, which identify a set of objects and axiomatize the functions for creating those objects and accessing the data associated with them.

Here is an example, assuming there is one type of agent holding a public-private key pair.

TYPESPEC PPK;
TYPES PKUser: Principal;
FUNCTIONS
  pk(PKUser): Pkey;
  sk(PKUser): Pkey,CRYPTO,PRIVATE;
VARIABLES
  A: PKUser;
AXIOMS
  keypair(pk(A),sk(A));
END;

Functions may be declared with a PRIVATE property when they are computed using data that is local to a principal. Private functions have a first argument identifying the principal who can access that "row" of the function. Thus, since the secret key function sk is private, the value sk(A) is available only to the agent A. In particular, the attacker can only see sk(X), where X is some agent identity owned or compromised by the attacker. Furthermore, it would be an error for a protocol specification to indicate that sk(A) is used in an action or transmitted message by a principal in a different role, say B.

Environment Specification

When a protocol is being analyzed or simulated, the analyst may have to specify which agents are to be run. The analyst may also have to supply other run-specific information such as the initial knowledge of the attacker. It was envisioned that CAPSL specifications could include ENVIRONMENT specifications containing this kind of information. (See Appendix B.3 of the CAPSL document.) ENVIRONMENT specifications are outside the PROTOCOL specification, like typespecs.

The content and interpretation of an ENVIRONMENT section depends on the analysis tool. However, it seems desirable for CAPSL to provide syntax, keywords, and organization so that different tools can at least take advantage of the CAPSL parser.

Declarations to name principals and other constants could be placed in this section. For example, suppose we want two principals, Alice and Bob, taking different roles in each of two sessions. We might set that up like this:

ENVIRONMENT Test1;
  IMPORTS PPK, NSPK;
  CONSTANTS
    Alice, Bob: PKUser;
    Mallory: PKUser, EXPOSED;
  AGENT Alice1 HOLDS
    A = Alice;
    B = Bob;
  AGENT Bob1 HOLDS
    A = Bob;
  EXPOSED
    {Bob}sk(Alice);
END;

Agents are specified here by assigning constants to protocol variables whose values are initially held by that agent. The first assignment must be to the owner variable. Nonces could be assigned values here or not, depending on the needs of the analysis tool.

The initial knowledge of the attacker is in the EXPOSED section. This would normally be a list of terms that the attacker is assumed to hold initially, possibly including some items that are declared in the protocol as secret. The attacker may be implicitly assumed to hold agent names.

A principal with an EXPOSED property is one whose private data is all held initially by the attacker. In this example, if Mallory is EXPOSED, sk(Mallory) is assumed to be compromised, and it would not have to be added to the EXPOSED list.

The constants Alice1 and Bob1 are of type Agent. Agents are, by default, assumed to run concurrently. CAPSL permits an "ORDER" section to specify some series-parallel sequencing of agents, for the benefit of search tools that could save time when such a restriction is assumed. For example, we might say: ORDER (Alice1;Alice2)||Bob1 to mean that session Alice2 does not start until Alice1 ends, but that sequence runs concurrently with Bob1.

An environment specification may have an AXIOMS section for assumptions about its constants, e.g., sk(Alice) = SKa.