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.
Last updated: July 17, 2006
Send comments and questions to ma@kestrel.edu, dusko@kestrel.edu. For more information, see also Dusko's homepage
