next up previous
Next: An example of verification Up: Validation process Previous: The verification toolbox

The verification


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 tex2html_wrap_inline732 where S is the set of states, A the alphabet of actions (with i denoting the internal action), T the set of transitions and tex2html_wrap_inline742 the initial state.

A relation tex2html_wrap_inline744 is a strong bisimulation iff:

If tex2html_wrap_inline746 then, tex2html_wrap_inline748,
whenever tex2html_wrap_inline750 then tex2html_wrap_inline752: tex2html_wrap_inline754 and tex2html_wrap_inline756;
whenever tex2html_wrap_inline754 then tex2html_wrap_inline760: tex2html_wrap_inline750 and tex2html_wrap_inline756

Two LTS tex2html_wrap_inline766 and tex2html_wrap_inline768 are related modulo the strong bisimulation denoted tex2html_wrap_inline770, iff there exists a strong bisimulation relation tex2html_wrap_inline772 such that tex2html_wrap_inline774.

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 (tex2html_wrap_inline776) is the preorder that generates the safety equivalence (tex2html_wrap_inline778), and is nothing else than the weak simulation preorder.

Consider again a tex2html_wrap_inline732 and let's define tex2html_wrap_inline782, a relation tex2html_wrap_inline744 is a weak simulation iff:

If tex2html_wrap_inline746 then, tex2html_wrap_inline788,
if tex2html_wrap_inline790, then tex2html_wrap_inline752: tex2html_wrap_inline794 and tex2html_wrap_inline756

A LTS tex2html_wrap_inline766 can be simulated by tex2html_wrap_inline768, denoted tex2html_wrap_inline802, iff there exists a weak simulation relation tex2html_wrap_inline772 such that tex2html_wrap_inline774. Two LTS tex2html_wrap_inline808 and tex2html_wrap_inline810 are safety equivalent iff tex2html_wrap_inline802 and tex2html_wrap_inline814.

Informally, ``behaviour tex2html_wrap_inline776 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.

next up previous
Next: An example of verification Up: Validation process Previous: The verification toolbox