Protocol Descriptions
The general idea is that protocols in Pda are described as abstract
entities and that certain projection functions exist that further
characterize the protocol. For instance, a simple Challenge-Response
protocol may be abstractly defined by the term CR[A,B](c,r) which
means that the protocol name is CR, the principals
(or agents) are A and B, and that the protocol has two
function variables c for the challenge and r for the response
function. If the developer wishes to define the behavior of this
protocol more precisely, he or she can define the actions of the
protocol and the partial order between them defining the “desired
run” of the protocol. This information is captured by providing a
projection function process and providing a definition term
for the abstractly specified protocol. In Pda, the process
description of a protocol is the core projection function for
protocols and therefore often referred to as the definition of the
protocol.
The Pda protocol language consists of textual as well as graphical elements for describing the entities of the protocol derivations. The graphical elements used are nodes and arrows representing connections between a pair of nodes. Nodes can be nested, i.e., a node can be a child of another node. Graphically this means that the outline of the child node is fully contained within the outline of the parent node. Nodes as well as arrows haves text labels. The following extensions to the EBNF grammar notations are used to represent those relationships:
LN |
represents a graphical node with label L and graphical N elements N. N must reduce to a list of nodes and arrows. |
*<L ` |
N<sub>1</sub> -> N<sub>2</sub>>`* |
N1 and N2 |
Using this notation, the description of a protocol is given by the following excerpt of the Pda protocol language:
ProtocolNode |
::= | ProtDecl |
( AgentNode ` |
The label of the protocol node obeys the following syntax rules, where
the notation “...” means that the definition of this non-terminal
contains more alternatives than shown in this particular rule
ProtDecl |
::= | SimpleProtDecl |
| ` | ||
SimpleProtDecl |
::= | ProtocolNameIdentifier |
[ StaticParams ] [ FunctionParams ] |
||
StaticParams |
::= | '[' AgentNameIdentifier |
(',' AgentNameIdentifier)* ']' |
||
FunctionParams |
::= | '(' FunctionNameIdentifier |
(',' FunctionNameIdentifier)* ')' |
||
ProtocolNameIdentifier |
::= | <capitalized identifier> |
AgentNameIdentifier |
::= | <capitalized identifier> |
FunctionNameIdentifier |
::= | <lower case identifier> |
An example of a SimpleProtDecl would be the abstract
representation of the Challenge-Response protocol as mentioned above:
“CR[A,B](c,r)”.
As specified in the rule for the protocol declaration, the agent nodes are used to specify the principals of the protocol. An agent itself is described by a state machine that specifies the agent’s behavior. This state machine is expressed using nodes and arrows between them; the arrows carrying local agent action information.
AgentNameIdentifier |
||
AgentNode |
::= | ( StateNode ` |
< AgentAction ` |
||
StateNode |
::= | < empty >< empty > |
AgentAction |
::= | 'new' VariableIdentifier |
| ` | ||
| ` | ||
| ` | ||
VariableIdentifier |
::= | <lower case identifier> |
ActionVariableIdentifier |
::= | <lower case identifier> |
The Pda protocol language defines the following set of terms that can be used in local agent actions as well as the payload of the send/receive messages, the syntax of which is defined further below:
Term |
::= | VariableIdentifier ( '[' AgentNameIdentifier ']' )? |
| ` | ||
| ` | ||
| ` | ||
| ` | ||
FunTerm |
::= | FunctionNameIdentifier [ AgentArgs ] [ Args ] |
InfixOp |
::= | `’+' |
AgentArgs |
::= | '[' AgentNameIdentifier |
(',' AgentNameIdentifier)* ']' |
||
Args |
::= | '(' [ Terms ] ')' |
Terms |
::= | Term (',' Term )* |
The send/receive arrows represent the message exchange between the agents of the protocol. In their basic format they just contain the payload in form of a term or a list of terms as specified above. In general, the send/receive arrow can also contain data for the sender and/or receiver field of a message; this is used, for instance, to model an intruder who manipulates the original message in order to sham the honest protocol principal. Another use of the explicit sender/receiver field is the “trusted-third-party” protocol, where the agent representing the trusted third party receives and sends the messages with the actual sender/receiver information. The syntax for the send/receive messages is as follows:
SendReceive |
::= | [ SenderReceiverAgents ':' ] |
Terms `[ ' |
||
SenderReceiverAgents |
::= | AgentNames '->' AgentNames |
AgentNames |
::= | AgentNameIdentifier (',' AgentNameIdentifier )* |