Before any comparison between LTS, they must be minimized to speed up the computations. The Aldebaran tool can minimize a LTS modulo a particular equivalence. The first minimization is always done modulo the strong bisimulation equivalence, which preserves all the properties of the graph.
Consider a 
where S is the set of states, A the
alphabet of actions (with i denoting the internal action), T the set of
transitions and 
the initial state.
A relation 
is a strong bisimulation iff:
If 
then, 
,
whenever 
then 
:
and 
;
whenever then 
:
and
Two LTS 
and 
are related modulo the strong bisimulation denoted 
, iff
there exists a strong bisimulation relation 
such
that 
.
Our security properties being all safety properties, the minimization can be further improved modulo the safety equivalence [BFG91], which preserves all the properties expressible in Branching time Safety Logic (BSL).
Not all the observable actions are relevant to verify the properties. In
particular, our properties only rely on special events, so that other actions can be
hidden. The minimized LTS of our protocol can be checked against the LTS of a
property be verifying the safety preorder relation [BFG91] between
them. Formally, the safety preorder (
) is the preorder that generates the
safety equivalence (
), and is nothing else than the weak simulation preorder.
Consider again a and let's define 
, a
relation is a weak simulation iff:
If then, 
,
if 
, then :
and
A LTS can be simulated by , denoted 
, iff there exists a
weak simulation relation such that
. Two LTS 
and 
are safety
equivalent iff and 
.
Informally, ``behaviour property'' means that the behaviour (exhibited
by the protocol) is allowed (i.e. can be simulated) by the (safety) property.
When a property is not verified, meaning that Aldebaran has not found a safety preorder between the LTS of protocol and the LTS of the property, it produces a diagnostic sequence of actions. However, this sequence is usually of little help as such, because it only refers to the few non hidden actions that were kept for their relevance to express the properties. We call it the abtract diagnostic sequence.
To circumvent this difficulty and get a detailed sequence with all actions visible, we have to encode this abstract diagnostic sequence in a format suitable for input to the Exhibitor tool. This tool is then instructed to find the shortest detailed sequence allowed by the specification and matching the abstract one. We are then able to clearly identify the scenario that leads to the undesirable state where the property is not verified. Intruder's attacks can then be pointed out very easily. The complete diagnostic sequence shows the order of actions performed by the intruder and how he was able to acquire enough knowledge to succeed.
The verification process of the properties is then complete. If one or more of them are not satisfied, our method gives diagnostics of a greatful help to redesign the protocol.