Rules

This description is preliminary. Please expect changes because the design of Rules and Constructors is an active research effort.

Rules are a more general form of Constructors. The latter take one (or more) protocol(s) as input and provide a form of specialization. (See Section @@ for examples of Constructors.) Rules operate on two or more protocols to combine them in a desired manner. A good model is the case of mutual authentication. Think of such a protocol as either nested or sequential challenge-response (CR) protocols. A rule can be built to compose two instances of a CR protocol into the desired mutual authentication result.

If you open a rule in the Database browser, you will see two additional component entries: Rule Argument and Rule Result. The idea is that you define a number of rule arguments representing pattern of the protocols you want to apply the rule to, and exactly one rule result, which represents the combination of parts of the rule arguments and possibly new parts.

• Applying a rule
• Creating a rule