Sequential compositionExampleEntering a protocolCreating an instance

Creating an instance

The simplest derivation step is protocol instantiation. Using the Create New Instance command (right-click on the CR protocol), some (or all) of the function variables can be refined to concrete primitives or other function variables. For example, we can get a one-way challenge-response protocol using nonces and signature as an instance of CR[I,R](c,r) with the following instantiation: c(x,y,z)=z, r(x,y,z)=Sig(y,z,x), where Sig is a signature function. You enter this instantiation in the editing dialogue that is presented once the instance has been created.

In the resulting protocol SCR[I,R], agent I sends a fresh nonce to R who replies with his signature over the nonce and I's identity.

Notice that the figure illustrates having collapsed the Template and expanded the instance.
Last updated: July 17, 2006
Send comments and questions to ma@kestrel.edu, dusko@kestrel.edu. For more information, see also Dusko's homepage

Sequential compositionExampleEntering a protocolCreating an instance