next up previous
Next: Handling unbounded nondeterminism Up: Using the ASTRAL Model Previous: Introduction

Overview of ASTRAL and ASTRAL model checker

An ASTRAL specification includes the global specification and process specifications. The global specification contains declarations of process instances, global constants and nonprimitive types that may be shared by process types, and system level critical requirements. There is a process specification for each process type declared in the global specification. In the Needham-Schroeder public key protocol specification, three process types are declared in the global specification:

        Initiator: array [ 1..NumberInitiator ]  of ProcessInitiator,
        Responder: array [ 1..NumberResponder ]  of ProcessResponder,
        Intruder: ProcessIntruder

This indicates that there are NumberInitiator initiators in the model of the protocol, each of process type ProcessInitiator. There are also NumberResponder precesses of type ProcessResponder and there is one Intruder process.

In the process specification of ProcessInitiator there are two parameterized transitions declared:

        TRANSITION Initiate ( j: RESP_INTR_ID )


        TRANSITION Receive ( j: RESP_INTR_ID )

where parameters i and j are of RESP_INTR_ID type, which basically comprises all identifiers of process instances of ProcessResponder and ProcessIntruder. The type ID is one of the primitive types of ASTRAL. Each process instance has a unique identifier and "self" is used to refer to its own identifier. The body of an ASTRAL transition includes pairs of Entry/Exit assertions with duration of each pair indicated. Entry assertion must be satisfied at the time the transition starts, whereas the Exit assertion will hold after the time indicated by the duration when the transition triggers. For example,

        TRANSITION Receive ( j: RESP_INTR_ID )
        Entry			[Time:1]
               	state = init
                & = self
                & Intruder.from = j
                & Intruder.pkey = PublicKey ( self ) 
                & Intruder.nonce_a = nonce_a
                & Intruder.source = self
                & Intruder.kind = Msg_Type_2 
                state = commit_inter
                & nonce_b = Intruder.nonce_b
                & pkey = PublicKey ( j ) 
                & to = j
                & from = self
                & kind = Msg_Type_3
                & source = self

which says if current state is init and the message on the network (modeled as process instance Intruder) encrypted in its own public key and of type Msg_Type_2, then after duration 1 time unit, the Exit assertion is satisfied with the state changes to commit_inter and a new message of type Msg_Type_3 is put on the network. The value of Intruder.kind in the Entry assertion is that of variable kind of process instance Intruder at the time when the transition fires. And source = self in the Exit assertion states that after 1 time unit, the value of variable source may change and the value should satisfy source = self.

ASTRAL specifications also include environmental assumptions and critical requirements. An environment clause formalizes the assumptions that must always hold on the behavior of the environment to guarantee some desired system properties, see [CGK97] for a detailed description of ASTRAL.

One way to verify an ASTRAL specification is with an ASTRAL model checker. However, due to the undecidability of ASTRAL which we will discuss further, several restrictions will apply to the specifications the model checker can handle.

The model checker procedure is composed of the following steps:

The basic task of the model checker is to verify, given a snapshot of current global state, the satisfiability of the ASTRAL specification critical requirements. The evolution of the ASTRAL abstract state machine is simulated within the given time bound to detect any violation.

The model checker is integrated to the ASTRAL SDE, coded in C++ with graphical user interface, running on Sun SparcStation 4 with UNIX Solaris 2.5.1.

next up previous
Next: Handling unbounded nondeterminism Up: Using the ASTRAL Model Previous: Introduction