next up previous
Next: Analysis of cryptographic protocols Up: Using the ASTRAL Model Previous: Overview of ASTRAL and

Handling unbounded nondeterminism

An ASTRAL specification has only finite process instances and each process instance has finite transitions. The initial statement of a process and the exit assertion of transitions may involve unbounded nondeterminism. For example, in modeling nonce generation of a security protocol like Needham-Schroeder's , we use the following transition in process ProcessInitiator:

        TRANSITION Initiate ( j: RESP_INTR_ID ) 
        ENTRY   		[TIME:1]
                state = idle 
                state = init
                & nonce_a = nonce_a
                & to = j
                & from = self
                & pkey = PublicKey ( j ) 
                & source = self 
                &  kind = Msg_Type_1

which among other things prepares a nonce_a for initiating the protocol. The EXIT assertion says after firing the transition with duration 1, nonce_a could be any fixed value from its domain as declared which certainly satisfies nonce_a=nonce_a. Hence the nondeterministic choices of nonce_a's value are unbounded provided it is of type integer.

The expressibility of ASTRAL formulas shown as invariant statements etc., is the same as PA (Peano Arithmetic), therefore the validity of ASTRAL formula is undecidable. This adds extra difficulties in handling the unbounded nondeterminism. In our model checker, we restrict the ASTRAL formula $F(\vec X)$ to the following generalized form (or equivalent):

\forall \vec y_1\exists\vec y_2\cdots Q\vec y_n I(\vec y_1\cdots \vec y_n,\vec X)\end{displaymath}

(Q is $\forall$ if n is odd and is $\exists$ otherwise.) where I is an arithmetic expression and $\vec y_1\cdots \vec y_n$ are either explicitly bounded or their bounds can be resolved by context. $\vec X$ is composed of local variables or exported variables from other process instances. Without loss of generality, assume $\vec X$ are exactly those variables which can not be resolved to deterministic value (otherwise we just hide them away). Furthermore, we restrict an Exit assertion to the following form:

$E=E \& E\vert E or E\vert\neg E\vert A\gt A\vert A<A\vert A=A\vert A<=A\vert A\gt=A

The atomic assertion A in the formula above is defined by,




In the formula above, C holds all deterministic values including exported variables P.X from another process P, constant expression n , and X' (the value that holds for X before starting the transition). All the other variables $\vec X$ are supposed to be changed after the transition. Without loss of generality, let $E(\vec X)$ stand for any Exit assertion as above. Define the Boolean structure $B_E$ as follows:


$B_{E_1 ~or~E_2}=B_{E_1}~or~B_{E_2}$

$B_{\neg E}=\neg B_E$


where $b_A$ is a Boolean variable indexed by A . Let $\vec b_A$ denote all Boolean variables in $B_E$ and define $\vec b_A(\vec X)$, an assignment of $\vec b_A$ according to $\vec X$, as $\vec b_A(\vec X)=A(\vec X)$.


             ((X=Y+1) or (Y=Z)) & X>Z

whose Boolean structure is

$(b_0 ~or~b_1)~\&~b_2$

For $<X,Y,Z\gt=<3,1,1\gt$, the $\vec b_A$ will be $<b_0,b_1,b_2\gt=<F,T,T\gt$.

Say $B_E(\vec X_1)=B_E(\vec X_2)$ if $E(\vec X_1)=E(\vec X_2)$ and $\vec b_A(\vec X_1)=\vec b_A(\vec X_2)$.

Denote $S(E)\subseteq S$ to be the solution space of $\vec X$ with $S(E)=\{\vec X:E(\vec X)=TRUE\}$.

Define $S/E(\vec X)$ to be a partition of S(E) :

(1). $\forall \vec X\in S, E(\vec X)=TRUE\iff \vec X\in \cup(S/E(\vec X))$,

(2). $\forall \vec X_1,\vec X_2\in S,
E(\vec X_1)=E(\vec X_2)=TRUE\land B_E(\vec X_1...
 ...(\vec X_2)\iff \exists S_0\in S/E(\vec X), \vec X_1\in S_0\land \vec X_2\in S_0$.

THEOREM. $S/E(\vec X)$ is finite.

Let S(F) be the solution space of F .

THEOREM. $S(E)\subseteq S(F)$ is undecidable.

Based upon these theorems, the best thing we can do with the model checker is to check F by guessing the solution as follows:

Let $\{\vec X_1,\cdots,\vec X_k\}$ be samples chosen from $S_i\in S/E(\vec X)$. Check F with these $\vec X_1,\cdots,\vec X_k$ respectively. F may be satisfied by these values but it may fail with other possible values. Because of the undecidability, in general we can't detect this failure. Hence by this algorithm, each transition branches into finite successors.

next up previous
Next: Analysis of cryptographic protocols Up: Using the ASTRAL Model Previous: Overview of ASTRAL and