Each system is ideally composed by two sections: in the first one you have to declare the identifiers that will be used in the rule definitions, in the second one you actually have to define the rules you wish to be tried during the protocol analysis. Each rule has a name, an associated identity, which represents the identity of the principal currently executing the corresponding instruction, a set of conditions that have to be satisfied in order to apply the rule, a set of actions to be executed if the conditions are satisfied. Each rule applies to a specified instruction with a given set of parameters. A generic rule has this shape:
rule A_RULE(I) { { instr(p1, p2, p3) } conditions { /* condition definition */ } actions { /* action definition */ } }
A_RULE
represents the name of the rule, I
the associated identity [1], instr
is
the name of the instruction which the rule is defined on, and pi
represent the instruction parameters. Parameters and identities are
identifiers, so they must have been declared in the apposite section;
the assignable types [2] are those used in the following
example:
declarations { Principal I, J; Variable p, p1, p2; // there is difference between names and variables Name p3; Key sk, ak; }
as you can see, it is possible to insert comments with the classic
C/C++/Java syntax: the double slash //
comments every character
until an end-of-line character is found; moreover every character included
between /*
and */
is ignored.
Containers model both typing environments and effects: each
action or condition is defined on containers. Each container
has to be defined in the relative section, preceding the declarations
one:
containers { ContainerType c1; ContainerType c2; }
ContainerType
identifies the name of the container type,
while c1
is the name of the container itself; four container
types are already provided with tool [3], while other
may be defined as plug-ins.
Each container has a standard operation set [4], whose elements may be invoked in the condition or action definitions [5]:
rule A_RULE(I) { { instr(p1, p2, p3) } conditions { /* condition definition */ } actions { c1.add(p1); c1.add(p2); c1.delete(p3); } }
The condition definition is a little bit more complex because a condition is made up of ipothesis-thesis couple in order to model the implication operator; the ipothesis is optional and if not defined is assumed to be true. Conditions may be defined as follows:
rule A_RULE (I) { { instr(p1, p2, p3) } conditions { ipothesis(c1.contains(p1)); thesis(c1.contains(p2) & !c1.contains(p3)); thesis(c1.contains(p2)); } actions { /* action definition */ } }
the example shows that it is possible to combine the results of the
single operations through the common boolean operators &
(and), |
(or), !
(not); if all the conditions
return true
or there are no conditions defined, actions
are performed.
Tags play a fundamental role in the validation algorithm: in fact both the rule systems provided with PEAR define a tag set. The tag definition is a crucial operation, because it has an impact on the behaviour of both protocol and rule parsers and, of course, on the tag inference algorithm. A message can not contain more than one tag for each type [6], moreover all the generic tags appearing in the same definition are mutually exclusive [7]:
tags { IdentityTag id; Tag claim, verif; }
the tag declaration is the last one and follows the identifier declaration. After declaring them, it is possible to tag identifiers as you wish:
rule A_RULE(I) { { instr({p1:claim, p2:verif, p3}:sk) } // this is an error }
the example above is wrong, because two tags defined together appear in the same message; it would be correct if the tag declaration had been:
tags { IdentityTag id; Tag claim; Tag verif; }
Instruction parameters may be simple as well as tagged identifiers, messages and instructions. The relative syntax states that a message is composed by an optional name, followed by a sequence of identifiers and an encryption or decryption key:
// p1 is a ciphertext encrypted with the symmetric key sk p1 = {I:id, p2}:sk // p2 is a ciphertext encrypted with the public part of key ak p2 = {|p3|}:Pub(ak) // a ciphertext decrypted with the private part of key ak {|p3|}(:Priv(ak))
provided that operations are nothing else than instructions defined on containers, they have the same syntax; thus it is legal to write:
rule A_RULE(I) { { instr({I:id, p1:claim, p2}:sk) } actions { c1.add(instr({I:id, p1:claim}:sk)); c1.add(instr(p2)); c2.add(p3); } }
since parameters may be seen even as containers, it is possible, for example, to check the content of a message, treating it as a container:
rule A_RULE(I) { { instr(p2 = {I:id, p1:claim, p3}:sk) } conditions { thesis(p2.contains(p3)); // true thesis(p3.contains(p2)); // false thesis(p3.contains(p3)); // true } }
Eventually it is possible to assign a text value to an identifier using the following syntax:
rule A_RULE(I) { { instr(p) } actions { c1.add(p="identifier") } }
While defining a rule system it is useful to remember that a sequential process is characterized by a signature, possibly declaring identities and keys, and a closing instruction, the null instruction:
A > Initiator(B:Id, k:sym-key(A,B)) := … .0
if a validation rule for the null instruction is not provided, it is impossible to complete the validation process successfully; the recommended definition of the null rule is:
rule NIL(I) { { 0 } }
this definition instructs PEAR to do nothing in presence of the null instruction, in fact there are no conditions or actions defined: this rule always validates the null instruction; obviously you can always provide a definition that suits better your needs. It is also possible to define rules that validate the signature declarations:
rule IDENTITY_DECL(I) { { id(J) } } rule SYMMETRIC_KEY_DECL(I) { { let(k = sym-key(I, J)) } }
the pseudo-instructions id and let have the function of providing an "access" to the signature declarations [8]; the rules defined in the above example do nothing and are not compulsory, because the signature is not an instruction of the protocol, but they may reveal useful in case one wishes to handle the containers' content to reflect the signature declarations. You should be aware that, once defined any condition in the above rules, the validation process may fail even at signature level.
To provide an operational support to the widest range of definable
rule systems, the ideal approach is allowing PEAR's functionalities
to be extended by means of plug-ins. Extensibility works in
two directions: new containers may be provided through classes overriding
the standard containers' behaviour [9] or providing
new operations; new single operations may be provided through classes
implementing the ExternalOperation
interface [10]; these may be applied to any container;
Operations defined by the container are called native
,
while stand-alone operations are called external
.
You may use a new container NewContainer
[11]
simply inserting its name in the related declaration:
containers { NewContainer nc; /* further declarations */ }
now you may use the operations defined on the new container exactly as explained previously (as a matter of fact the containers provided with PEAR are plug-ins):
nc.natop(p)
If you wish to invoke an external operation on a container you need to specify that the operation must not be looked for among the ones defined by the container; this may be done at three levels:
actions { (external)c1.extop(p); }
conditions { ipothesis(c1.contains(p) & c2.contains(p)); external thesis(c1.extop(p) & c2.extop(p)); }
rule EXT_RULE(I) { { instr(p, p1) } external conditions { ipothesis (c1.extop(p1)); thesis(c1.extop(p) & c2.extop(p)); } external actions { c1.extop(p2); c2.extop(p2); (native)c2.add(p1); // this operation is native } }
moreover, everywhere you may use the external
keyword,
you may also use the native
complementary keyword with
opposite meaning.
The rules are associated to the instruction appearing in the protocol encoding trough pattern-matching. The rho-spi syntax is translated in the one used by the rules, thus letting an instruction to match exactly the shape defined by the associated rule:
decrypt xT as {nA:verif, B:id, kAB}:kAT.
is translated to:
decrypt(xT={nA:verif, B:id, kAB}(:kAT)).
so, by defining an appropriate rule, it is possible to validate the
previous decrypt
primitive:
rule A_DECRYPTION(I) { { decrypt(p={J:id, p1:verif, p2}(:k1)) } actions { /* action definitions */ } }
in this case, being A
the principal executing the sequential
process, the substitution map will have the following content:
[I=A, p=xT, p1=nA, J=B, p2=kAB, k1=kAT]
all the free identifiers appearing in the rule are mapped on the ones
placed in the corresponding positions in the instruction, with an exception:
the order of the components of a message is immaterial. Since it is
unpredictable the number of identifiers with no tags appearing in a
message, you may use the dots construct (…
) to match them:
rule A_MORE_GENERAL_DECRYPTION(I) { { decrypt(p={J:id, p1:verif, ...}(:k1)) } actions { /* action definitions */ } }
this version handles a definitely wider range of cases:
decrypt xT as {nA:verif, B:id, kAB, z}:kAT. [I=A, p=xT, p1=nA, J=B, ...=[kAB, z], k1=kAT]
the dots construct may be placed everywhere you may find a simple identifier. The colons construct matches both tagged and untagged identifiers, and may be used in the same way as the dots construct:
rule THE_MOST_GENERAL_DECRYPTION(I) { { decrypt(p={:::}(:k1)) } actions { /* action definitions */ } }
this version handles all the cases:
decrypt xT as {nA:verif, B:id, kAB, z}:kAT. [I=A, p=xT, :::=[nA:verif, B:id, ...], ...=[kAB, z], k1=kAT]
Every mapping is kept when passing to the condition evaluation; this means that all the identifiers that have already a mapping are overridden with their mapped value, while the free ones are subject to the auto pattern-matching algorithm, which provides a form of universal quantification: for each operation the related container content is checked, looking for new possible mappings to add to the substitution map: the process is strictly sequential and checks each element of the container. The algorithm makes successive attempts to find the right mapping, exploiting the underlying backtracking mechanism, until a correct mapping can be found or the whole container has been checked. Considering the previous example, the algorithm will work as follows:
rule THE_MOST_GENERAL_DECRYPTION(I) { { decrypt(p={:::}(:k1)) } conditions { thesis(c1.contains(k1=sym-key(I,J))); } actions { c2.add(decrypt({:::}(:k1))); } }
the previous substitution map will lead to an operation defined as follows:
c1.contains(kAT=sym-key(A,J))
supposing that the container c1
has the following content:
c1=[kBT=sym-key(B,T), kAT=sym-key(A,T)]
To a human observer may be obvious that the missing mapping is J=T
,
but the validation core has no idea of the meaning of the contains
operation. It tries then to match the first element of c1
,
failing because it should insert in the substitution map the element
kAT=kBT
, while the identifier kAT
is already
bound. Hence the validation core tries to match the second element obtaining
the correct mapping J=T
. If the condition evaluation is
successful, then the actions are performed: in this case operations
will be instantiated according to the substitution map content, but
there will be no further pattern-matching. You may exploit conditions
to perform a "void" auto pattern-matching through the external (hence
defined on all the containers) operation match
, which has
no influence on the condition evaluation because it always returns true
:
rule THE_MOST_GENERAL_DECRYPTION(I) { { decrypt(p={:::}(:k1)) } conditions { thesis(c1.contains(k1=sym-key(I,J))); external thesis(c2.match(n="identifier")); } actions { c2.set(n="identified"); c2.add(decrypt({:::}(:k1))); } }
if c2
does not contain an element that may be associated
to n, then the action will be executed using n
as actual
parameter, else the substitution map will be updated as needed:
c2=[id="identifier"] c2.set(id="identified") c2.add(decrypt({nA:verif, B:id, kAB, z}(:kAT))) c2=[id="identified", {nA:verif, B:id, kAB, z}(:kAT)]
To configure the validation process, three directives are available: the first one is directed to the auto pattern-matching algorithm, the other two to the backtracking handler.
@ra
is used to temporary reset the association of
the dots construct in the substitution map, which may result useful
in certain situations; it must be placed before a condition clause
and it scopes the whole clause:
rule A_RULE(I) { { instr(...) } conditions { ipothesis(c1.contains({...}:k1)); @ra thesis(c2.contains(p={...}:k2)); } actions { /* action definitions */ } }the dots construct appearing in the ipothesis clause will be substituted with the value taken from the map, the one appearing in the thesis clause is subjected to auto pattern-matching.
@exist
, @univ
are alternative and complementary
directives: they are used to alter the standard behaviour of the backtracking
handler; normally the validation core, in presence of an ipothesis
clause, applies an universal quantification policy. In this
case it tries to satisfy in every way the checks defined in the clause;
instead, in presence of a thesis
clause, the validation
core applies an existential quantification policy: a single
check's failure is enough to state the failure of the whole clause
evaluation. This causes the evaluation of all the conditions to fail,
because they are related by a boolean and operator. Usually
this behaviour is correct and sensible; if you wish to modify it for
any reason, then you may specify the desired directive before the
interested clause:
conditions { @exist ipothesis(c1.contains({...}:k1)); @ra @univ thesis(c2.contains(p={...}:k2)); }Obviously assigning to the clauses their default directives does not alter the behaviour of the backtracking handler in any way. As you may notice from the above example, directives have to be expressed in a precise order:
[@ra] [@exist | @univ] condition_clause
SetContainer
models a simple
set, OrdContainer
models an ordered container, MultisetContainer
models a multiset, MapContainer
models a set whose elements
have an associated value.add(p)
inserts the parameter
p
in the container, add(p, val)
inserts
the parameter p
in the container, associating to it the
value val
, contains(p)
checks if the element
p
is held in the container, while delete(p)
removes the element p
from the container.Tag
generic tag type, KeyTag
used to tag keys, TypeTag
used to type identifiers, NonceTag
used to tag nonce, MessageTag
used to tag messages, IdentityTag
used to tag identities, CiphertextTag
used to tag encrypted
messages.sym-key(A,B)
is equivalent to sym-key(B,A)
.Container
interface describes the set of standard operations.checkType
checks the type of a message.it.unive.dsi.pear.plugins
.