Let us start by defining a couple of simple processes.
SPEC> P := nu (x,y). a< enc(x,y) >.a<b> ;
SPEC> Q := nu (x,y). a< enc(b,y) >.a<b> ;
This defines two processes P and Q. We can use the command #show_defs to show the process definitions we entered so far:
SPEC> #show_defs;
P := nu(n1,n2).a.a<b>.0
Q := nu(n1,n2).a.a<b>.0
SPEC>
Notice that SPEC automatically renames the bound variables x and y to its internally generated fresh names (n1 and n2 in this case). In general, SPEC will prefix any bound names or names freshly generated with the letter ‘n’. The engine also performs α-conversion as neccessary to avoid name clashes.
As discussed in the previous section, free names in a process entered by the user are automatically considered as constants by SPEC, with the consequence that they are known publicly to the intruder.
Recall from Section 2 that the command bisim allows use to check for bisimilarity:
SPEC> bisim(P,Q);
Checking bisimilarity for:
nu(n1,n2).a<enc(n1,n2)>.a<b>.0
and
nu(n1,n2).a<enc(b,n2)>.a<b>.0
..
The two processes are bisimilar.
Size of bisimulation set: 2. Use #show_bisim to show the set.
Running time: + 0s
What the implementation of bisimulation in SPEC does is basically unfold the transitions of P and Q in locked steps, and at each step, the messages input/output by the processes are added to the current bitrace (initially, it is the empty bitrace). At each step, SPEC also checks that the bitrace produced in that step is consistent. The bisimulation set produced by SPEC can be displayed using #show bisim:
SPEC> #show_bisim;
1.
Bitrace: []
First process: nu(n1,n2).a<enc(n1,n2)>.a<b>.0
Second process: nu(n1,n2).a<enc(b,n2)>.a<b>.0
2.
Bitrace: [(enc(n1,n2), enc(b,n2))^o.]
First process: a<b>.0
Second process: a<b>.0
SPEC>
The original processes are listed in the first item, which get unfolded into the second item. In the second item, we notice that the first process is actually equal to the second process. SPEC recognises this automatically and stops the unfolding at this point, as bisimilarity is reflexive. The resulting bitrace at eachstep is also given. As we said earlier, input or output messages are appended to the current bitrace at each step.
1. Separation of names in bisimulation
An important thing to note in reading a bisimulation triple (h, P, Q) is that the names (other than constants) used in the first projection of the bitrace h and process P are unrelated to the names used in the second projection of h and Q. This is because names represent entities that may be generated internally by the processes (via scope extrusion) and may be unknown to the intruder, hence their identities are not something which is generally observable. See [AG98] for an explaination of this.
2. Equivariance of bisimilarity
Another important thing to keep in mind when reading the output bisimulation set produced by SPEC is that each triple in the set represents an equivalence class of triples modulo renaming of variables and names (but excluding constants). Thus, a triple such as
([(x, x)i.(enc(n, m1), enc(b, m2))o], P, Q)
where x is a variable, n and m are non-constant names and b is a constant, represents the set containing
([(xθ, xθ)i.(enc(nθ, m1θ), enc(b, m2θ))o], P θ, Qθ)
where θ is an renaming substitution.
3. Examples
We show here a simple but interesting example to illustrate features of the bisimulation output. The SPEC distribution contains a number of small and big examples in the directory examples. Some of these examples encode a number of security protocols. These examples may produce very large bisimulation sets (in the order of hundreds to more than a thousand elements) and may take quite a while to execute.
Example 1 Let
P1 := a(x).ν(k).a<enc(x, k)>.ν(m).a<enc(m, enc(a, k))>.m<a>
Q1 := a(x).ν(k).a<enc(x, k)>.ν(m).a<enc(m, enc(a, k))>.[x = a]m<a>
The process P1 inputs a term via channel a, binds it to x and output an encrypted message enc(x, k). It then generates a new channel m, sends it off encrypted with the key enc(a, k). Here the name a is a constant, so it is known to the intruder. The process then sends a message on the newly generated channel m. Although the channel m is a secret generated by P1, and it is not explicitly extruded, the intruder can still interact via m if it feeds the name a to P1 (hence binds x to a). As a result, the (symbolic) output enc(x, k) can be ‘concretized’ to enc(a, k), which can be used to decrypt enc(m, enc(a, k)) to obtain m.
The process Q1 is very similar, except that it puts a ‘guard’ on the possibility of interacting on m by insisting that x = a. The above informal reasoning about the behavior of P1 shows that it should be observationally equivalent to Q1.
Before we try proving the bisimilarity of P1 and Q1, first execute the following command:
SPEC>#reflexive off;
Reflexivity checking is disabled.
This instructs SPEC to disable an optimisation, i.e., the reflexivity checking. Reflexivity checking allows SPEC to conclude immediately that identical pairs of processes are bisimilar. Disabling this allows us to see a bit more clearly how the bitraces in the bisimulation set in the following example change from one entry to another
After disabling reflexivity checking and running the command bisim(P1,Q1), we get that the two processes are indeed bisimilar. The bisimulation set produced can be displayed using the #show bisim command, but here we shall try to output it in a LaTeX format:
1. Bi-trace: [ ]
First process:
a(n1).
ν (n2).
a < enc(n1, n2) >.
ν (n3).
a < enc(n3, enc(a, n2)) >.
n3 < a >.
0
Second process:
a(n1).
ν (n2).
a < enc(n1, n2) >.
ν (n3).
a < enc(n3, enc(a, n2)) >.
[n1 = a]
n3 < a >.
0
2. Bi-trace:
(enc(a, n1) , enc(a, n1))o.
(enc(n2, enc(a, n1)) , enc(n2, enc(a, n1)))o.
First process:
Second process:
3. Bi-trace:
First process:
ν (n2).
a < enc(?n1, n2) >.
ν (n3).
a < enc(n3, enc(a, n2)) >.
n3 < a >.
0
Second process:
ν (n2).
a < enc(?n1, n2) >.
ν (n3).
a < enc(n3, enc(a, n2)) >.
[?n1 = a]
n3 < a >.
0
4. Bi-trace:
(?n1 , ?n1)i.
(enc(?n1, n2) , enc(?n1, n2))o.
First process:
ν (n3).
a < enc(n3, enc(a, n2)) >.
n3 < a >.
0
Second process:
ν (n3).
a < enc(n3, enc(a, n2)) >.
[?n1 = a]
n3 < a >.
0
5. Bi-trace:
(?n1 , ?n1)i.
(enc(?n1, n2) , enc(?n1, n2))o.
(enc(n3, enc(a, n2)) , enc(n3, enc(a, n2)))o.
First process:
Second process:
A few notes on the output produced by SPEC:
- Typesetting of names and variables: Variables are typeset by prepending the variables with a question mark ‘?’. Bound names and non-constant names are typeset using italised fonts, while constants are un-italicised.
- The original process pair is given in item 1. The unfolding sequence proceeds as follows: 1 → 3 → 4 → 5 → 1. Notice that in moving from 5 to 1, the input pair disappears from the bitrace. This is because the variable ?n1 gets instantiated to a, which is a constant (hence, public knowledge), and it is removed by the simplification step of SPEC.
- Equivariance of bisimulation: Notice that in proceeding from 5 to 1 there is an implicit renaming performed by SPEC.(This automatic renaming is a built-in feature of Bedwyr, so it is not possible to alter it without modifiying the search engine of Bedwyr. It is a by-product of equivariance tabling implemented in Bedwyr. See Section 7.) Without renaming, the bitrace in item 1 would have been the following:
(enc(a, n2) , enc(a, n2))o.
(enc(n3, enc(a, n2)) , enc(n3, enc(a, n2)))o.