Entering a protocol
A protocol is a distributed program. To specify a protocol, you must specify a sequence of actions to be executed by every participant in the protocol. Actions divide into two groups: external actions, i.e., sending and receiving a message and internal actions, i.e., generating nonces, keys, hashes, decryption and other local computation. (For agent actions, note that the reserved terms are if, then, match and new. For full details on the language to describe actions, functions, and variables, please see the Reference Manual.)
Protocols are entered into Pda with the elements of the Protocol Toolbar. The program of every agent is a linear sequence of state descriptions (Stads), with transitions being either send, receive, or agent step (internal compuation).
The next figure shows where you are after creating a new protocol diagram called CR Template in your Browser and opening it for edit.
In the Editing pane, select Protocol from the Protocol toolbar, click in the Editing pane, and enter CR[I,R](c,r) to replace the default text (Unnamed_Protocol). Click outside the text area and you will see the next screen.
Double-click the collapsed icon to show/edit the protocol, (alternatively, you can right-click to expand it), and you find:
Now click on Agent Stad in the toolbar, then near the top of the Agent I box, then do the same steps again at the middle and then the bottom. You will see the next figure. Notice, after each placement of an Agent Stad, you must reselect the Agent Stad option from the toolbar. That’s where Quick Edit can save you time (see the Main panel section).
For now, let’s use a different aid, namely, Zoom. Click inside the protocol, between the two agents, to select it. Then type “z”. Return to the toolbar, pick Agent Step. Then click first in the top Agent Stad, release the mouse, position the cursor over the middle Agent Stad, and click/release again. In the window that appears, type “new m”, and click outside the agent. You can reposition text by selecting it and using your arrow keys, e.g., to produce the next figure.
Now use the toolbar items yourself to produce the following two party CR[I,R](c,r) protocol description. Don’t forget that you have to reselect toolbar items after each step. For example, when you want to reposition text, you must select Select.
In this protocol, Agent I (initiator) has the carried out the following sequence of actions: generate a new nonce m, send the message c(I, R, m) to R, receive a message r(I, R, m) from R. Correspondingly, Agent R (responder) receives a message c(I, R, m) from I and sends a message r(I, R, m) to I.
Messages exchanged in a protocol contain concrete cryptographic primitives such as encryption, signature and hash, and function variables such as c and r in this example. The only reserved term for these operations (at this time) is the keyword new. Other notations are up to the user. See the section Conventions for suggested usage.
When a protocol contains function variables, we say that it is a protocol template. In this example, the protocol header CR[I,R](c, r) should be read: CR is a two party protocol (agents are named I and R), using abstract function variables c and r.