Variables

For convenience of use, the diagrammatic protocol representation in Pda is set up to resemble, as much as possible, the informal protocol notation of “arrows-and-messages”. On the other hand, one of the main goals of this tool is to support formal reasoning about security. To balance between these two goals, for better or for worse, we use a generous set of graphic abbreviations and annotations.

The formal model underlying Pda has evolved through the papers available from www.kestrel.edu. Here we provide a brief summary.

A protocol specification consists of a process, a desired run, and a specification of its security properties. A process is specified as a multiset of agents, which may be the protocol principals, or attackers. Each agent is a program, i.e. a partially ordered multiset of actions. The actions can be internal or external.The internal actions include the usual computational operations, such as assignment and test; and the specific security operations, such as generation of random values.

The external actions can be:

• (send A->B:t), where A and B are constant agent identifiers, and t is a closed term; or
• (recv X->Y:z), where X and Y are agent variables, and z is a term variable

The sender denotes by A and B the purported source and destination of the message, which may or may not be the actual sender and receiver: an attacker can spoof these fields; a router can use them to direct traffic. The receiver denotes by X and Y the claimed source and destination of the received message, and by z its payload.

The desired run of a protocol is an assignment of a unique send action to each receive action. In Pda, this is denoted by drawing arrows between agents. In this way, the process and the desired run are specified together. However, this is a matter of convenience, and it should be clear that processes can have many different runs. In many cases, security means that undesired runs will be detected.

Connecting (send A->B:t) with (recv X->Y:z) in a run has the effect of simultaneously assigning X:=A, Y:=B and z:=t in receiver’s environment. In Pda, the source and the destination fields of these two actions are elided from the graphic display whenever they coincide with the actual sender and receiver of the actions linked in the run. Note that this is just a display feature: in the underlying formal model, the source and the destination fields are always present.

The variables that occur in the receive action are bound to the received values only when the process is run, i.e., dynamically. These variables are necessary to allow specifying statically (at design time), any computations that are to be undertaken at run time. Moreover, while the term structure of the received data (e.g., that it is encrypted by Alice’s key) may not be discernible to Bob, he can still manipulate such data, e.g., for passing it forward to a trusted third agent. This is illustrated in the following figure.

@@ create figure
@@ need figures and examples