|
|
| MuCAPSL |
|
|
|
MuCAPSL is an extension of CAPSL with language features to handle
protocols for secure group management. The main design issues
are multicast addressing, multiplicity of group tasks, variability of
group size, membership, and message sizes,
mutability of group information, and new computational
operators. The MuCAPSL Reference document
is SRI International CSL Technical
Report SRI-CSL-03-02, June, 2003 (postscript).
The new features of MuCAPSL include:
A MuCAPSL specification has typespec, protocol, and environment modules, like a CAPSL specification. In addition, MuCAPSL provides for the grouping of several protocols into a suite, and there are new keywords and structural concepts within the definition of typespecs and protocols. There are changes also in environment modules and goal specifications. The current MuCAPSL syntax is given in informal BNF. There is also a preliminary MuCAPSL Translator in Java, with an optional window interface. We will illustrate some of the new language features with the help of the Group Diffie-Hellman protocols that served as the basis for the Cliques protocol suite. In particular, we will use the key distribution protocol GDH.2 as an example, together with related protocols for member addition and deletion. For a more complex and complete example, look at the GKA specification. MuCAPSL uses a somewhat different prelude from CAPSL. Group Principal TypespecsGroup members are principals having mutable persistent group state attributes. Attributes are declared in a typespec for the particular group state architecture. |
| For example, a GDH.2 group member, which we shall identify with subtype GDHAgent of the standard type GroupMember, has an index within the group id, a secret nonce N, the current size of the group n, the current group key Kn, and arrays of "upflow" KU and "downflow" KD values. Attributes are associated with the declared GroupMember subtype by the ATTRIBUTES declaration, in the sense that each object of the named type has state variables corresponding to the attributes. Attribute values persist over protocol sessions and can be modified by actions within a protocol session. |
TYPESPEC GDH;
TYPES GDHAgent: GroupMember;
CONSTANTS g: Skey;
ATTRIBUTES
id: Nat;
N: Skey, FRESH;
n: Nat, INIT 0;
Kn: Skey;
KU: Sarray;
KD: Sarray;
END;
|
| A protocol suite is a syntactic unit containing one group principal typespec and one or more protocol specs for protocols which members of that kind of group can execute. GDH.2 might have protocols to start up a group with two initial members, a key distribution protocol, and protocols to add and delete members. A suite might also contain other declarations unique to a group and shared by the group protocols. |
SUITE GDH2;
TYPESPEC GDH;
...
END;
PROTOCOL StartUp;
...
END Startup;
PROTOCOL KeyDist;
...
END KeyDist;
PROTOCOL Add;
...
END Add;
PROTOCOL Delete;
...
END Delete;
END;
|
|
A significant difference between CAPSL and MuCAPSL is the separation
of roles in the specification. In a CAPSL protocol specification
the different roles must be inferred from messages like A -> B: C.
Role names are no longer bound syntactically to variable names A and B.
In MuCAPSL, actions are placed in different ROLE sections,
and messages are sent or received by the process in that role.
A message sent is "-> B: C" or "-> : C" depending on whether it is
unicast to B or multicast to the group, and "<- C" is a message
received by the process in the specified role.
In the GDH.2 key distribution protocol, for example, there are three roles: First for a group member with index 1, Last for the highest-numbered group member, and Mid for all others. |
PROTOCOL KeyDist;
ROLE First;
ASSUMPTIONS id = 1;
...
MESSAGES
-> : 2, g^N, g;
<- KD
Kn = KD[1]^N;
END KeyDist;
|
A process knows whether it can play a role by checking
some condition on its attributes, in this case id = 1 for
the First role. The sent message is an "upflow" which in
this version is multicast but contains a field implying a
condition to identify the intended recipient, in this case
the one with id = 2. (The intent to test `2' against id
is built into the protocol specification, in the Mid and
Last roles that receive upflow messages.
The received downflow message is multicast and contains
an array KD which each role uses differently to calculate
the group key.
Sequences and ArraysAn array like KD can be used as a message field and as the value of an attribute. Its ith element is KD[i], and an assignment action like KD[i]=1 can change an element value. Subsequences of array elements can selected and made into arrays with a new angle-bracket notation.
|
| In the Mid role of the KeyDist protocol, for example, a message is sent to the member with next higher id, containing modified upflow values extracted from the KU array. The message is preceded by a NEW action that generates a fresh value for the nonce N. The use of an elementwise exponentiation operator on the array KU is also illustrated here. |
... NEW N; -> : id+1, <<KU^^N>>, KU[1]; ... |
| An equality action in CAPSL like X = Y is either an assignment or a test, depending on whether the value of the variable X is already held. In MuCAPSL, X could be an attribute, and X = Y is ambiguous since attributes can be modified. Hence there is a new test prefix `?' indicating when an attribute value is to be tested rather than modified. Thus, ?X = Y is a test and X = Y, by default, is an assignment. |
| When an attribute appears in a received message, the test prefix has a similar role in deciding whether the received value is to be stored or used for a test. The default is to store the received value. In principle, a received message "<- X" is an action X = X' where X' is the message content. Thus, at right, X is stored and Y is tested for equality with the received value. It is unnecessary but permissible to use the `?' notation with protocol variables. |
<- X,?Y; |
| There are some cases involving arrays where the implications of the test prefix are not entirely obvious. We will not attempt to cover those here. |