Candidate conventions
This section provides possible conventions for protocol descriptions
in Pda. Users are free, of course, to use their own choices to
choose the notation used in a protocol description, as the examples in
this manual demonstrate.
- agent names A, B, C, ...
This image shows the engagement of two agents, A and B. Each agent's
internal activities, including accepted input and output produced,
will be illustrated in its respective column.
- server names: S, S1, S2,...
Protocols can also include a trusted third party, for example a key
server for authentication. This image shows the structure to build
when a server is part of the protocol. Note that the display of agent
activities follows the same order as listed in the argument to the
protocol name.
- agent action names: new, if, then, and match are reserved
words in Pda, and are the only action names currently supported.
An agent can carry out internal actions, e.g., generation of a nonce,
a timestamp, a clear text message, a key, etc. Internal action
reserved names include: new, if, then, match. Generic action result
names may be labeled q, q1, q2,... The image here shows creation of a
new datum labeled q.
- nonce names x, x1, x2, ... Nonces are fresh values used
typically in authentication protocols. One form of nonce is a
timestamp (see below), but many protocols simply prescribe a value
that is randomly generated.
- timestamp names ts, ts1, ts2,... Timestamps are an
alternative to nonces for authentication. They are used to prevent
replay as new of captured messages.
- clear text names t, t1, t2,... Clear text can include
items such as agent names, public keys, and non-sensitive text
messages. The following figure shows Agent A sending clear text along
with a shared key to Agent B.
- key function names K(), K[A,B](), K[B,S](),... Keys are
functions in Pda. The generic key reference is K(), but if the parties
sharing the key are named, the convention is to list them as arguments
in square brackets, as shown in this figure.
The function notation for arguments is empty when the key is the
payload. When a message payload includes encrypted text, it is
included in the key function's arugments. The following figure shows this
convention.
- hash function names H(), H[A,B](), H[B,S](),... Hashes
are functions in Pda. The generic hash reference is H().
- crypto variable names cv, cv1, cv2,...2
- names Protocol names are, of course, up to the designer.
For the ClarkJacob libraries, the numerical naming scheme was chosen
for convenient referencing into the paper. Intermediate protocols in a
derivation (also, Rule or Constructor) may be used by other
derivations, so some attention to their naming may be helpful. Give
some thought to picking names, since you will want to recognize
reference instances among possibly long lists of protocols in your
browser.
Last updated: July 17, 2006
Send comments and questions to ma@kestrel.edu, dusko@kestrel.edu. For more information, see also Dusko's homepage