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.