Protocol InstantiationsThe Pda Protocol Derivation LanguageProtocol Descriptions

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:

L
N
represents a graphical node with label L and graphical elements N. N must reduce to a list of nodes and arrows.
<L  | N1 -> N2 > represents a graphical arrow with label L connecting graphical nodes 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 | < SendReceive  |  StateNode ->  StateNode >)*

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.

AgentNode ::=
 AgentNameIdentifier
( StateNode | 
< AgentAction  |  StateNode ->  StateNode >) *
StateNode ::=
<empty >
<empty >
 AgentAction ::= `new' VariableIdentifier
 |  ActionVariableIdentifier
 |  VariableIdentifier `:=' Terms
 |  `if' Term `then' AgentAction
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
 |  `(' Terms `)'
 |  < number >
 |  Term InfixOp Term
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 `:' ] Terms ]
SenderReceiverAgents ::= AgentNames `->' AgentNames
AgentNames ::= AgentNameIdentifier ( `,' AgentNameIdentifier )*

Last updated: July 17, 2006
Send comments and questions to ma@kestrel.edu, dusko@kestrel.edu. For more information, see also Dusko's homepage

Protocol InstantiationsThe Pda Protocol Derivation LanguageProtocol Descriptions