Discussion

In ASTRAL two categories of critical requirements are explicitly distinguished, one is ASTRAL invariant clause, the other is ASTRAL schedule clause. The former will always hold regardless of the validity of environmental assumptions, while the later will hold if environmental assumptions are satisfied. Therefore, even if the current state constructed by the model checker does not satisfy the environmental assumptions, we still need to check the validity of invariant clauses. However, for the user's convenience, our model checker has the option of checking only the states satisfying the environmental assumptions. Therefore, if a user makes this choice when using the model checker, he could significantly reduce the search space by imposing stronger restrictions on the environmental assumptions of the specification without rewriting the specification.

The efficiency of using our model checker to analyze secure protocols is heavily dependent on the following factors:

• depth of the anticipated run of a protocol coded in ASTRAL. Different modeling methods differ dramatically. For example, our first version of Needham-Schroeder public-key authentication protocol specification, the message passing between two parties is not relayed by the network (the intruder): each participant including the intruder has local variable called Msg which can be seen by others under the condition that the observer can decrypt it. In the same manner, the intruder has the ability to accumulate his knowledge of other participants by overhearing and decrypting whenever he can, and to replay an old message or construct a malicious message which may fool an honest agent. Though this method may not work well in other cases, our test results show that the same bug is found within 62 seconds with 3600 states explored. In this case the time bound is only 7. However, this method produces a messy low level ASTRAL specification instead of a clean high level ASTRAL specification.
• avoid unnecessary exporting and idling of transitions . Exported transitions may cause "idling" if it's not called by external environment. That is, even though the entry assertion is satisfied, the transition is still not firable. We can not put firm restrictions on calls to exported transitions except as stated in the environment clause.
• using simple ASTRAL types. ASTRAL provides rich data types and their operations. However, complex types like List of List or List of Structure compositions need more time to resolve and more space to allocate.
• using fewer process instances and fewer transition instances in a specification. Like the examples in this paper, we combine the network with the process Intruder, in the sense that the intruder will fully control the network.

Our model checker missed a bug in TMN which is uncovered by FDR [LR97], because it required too large of a time bound under the current ASTRAL coding of the specification. The simpler bug shown in this paper is also uncovered by Mur$\varphi$[MMS97] .

Results presented in this paper are preliminary. As our experience specifying protocols in ASTRAL grows, we believe the results can be improved further. We intend to apply the model checker in investigating some real time protocols in which ASTRAL will show its advantages as a high level real time specification language.