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:

PROCESSES
        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 )

and

        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
                & Intruder.to = self
                & Intruder.from = j
                & Intruder.pkey = PublicKey ( self ) 
                & Intruder.nonce_a = nonce_a
                & Intruder.source = self
                & Intruder.kind = Msg_Type_2 
        Exit
                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:

• Assign a model checker time bound. ASTRAL abstract machine is, in general, an infinite state machine with unlimited time bounds whenever the system can evolve. However, in order to make the model checker work, a finite time bound needs to be set by the user.
• Place a call index I to exported transitions in the specification. According to ASTRAL semantics, an exported transition must be called by the external environment before it starts. The model checker will verify if such an index is suitable by checking that it satisfies the condition that for any exported transition T , a call need not be placed to it at current time if T was already called but has not yet started.
• Apply the call index to the current state and select an enabled transition index. Such selection should obey the ASTRAL semantics, which says at most one transition is firing for each process at any time, and a transition is enabled if its entry assertion is satisfied and no other transition in the same process instance is firing at the current time, also if it is an exported transition, it should be in the call index. Then by updating Call time and Start time of transitions in the two indices according to the combination of call index and enabled transition index.
• Evolve the system forward by applying the selected combination of call index and enabled transition index. Check and report any violation of the critical requirements.
• Evolve the system backward if we run out of call indices and enabled transition indices or the system time bound is reached.

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.