ASTRAL[GK91] is a high-level formal specification language for real-time system. It is provided with structuring mechanisms that allow one to build modularized specifications of complex systems with layering[CGK97]. A real-time system is modeled by a collection of process specifications and a single global specification. Each process specification consists of a sequence of levels; each level is an abstract view of the process being specified. In [CKM94] formal proofs in ASTRAL, which include interlevel proofs and intralevel proofs, are discussed and a formal framework for generating intralevel proof obligations in ASTRAL is presented. The potential unbounded nondeterminism in ASTRAL transition exit assertions and the validity of the critical requirement statements, which may involve quantifiers over unbounded ASTRAL types, make ASTRAL specifications undecidable. The ASTRAL model checker presented in this paper will be used to verify ASTRAL specification under some restrictions.
The ASTRAL Software Development Environment (SDE) is an integrated set of design and analysis tools based upon the ASTRAL formal framework, which includes a syntax-directed editor, a specification processor, a verification condition generator, and a browser kit. The ASTRAL model checker is added as a new component to the SDE. It checks satisfiability of critical requirements of an ASTRAL specification by enumerating possible runs of transitions within a given time bound. It prompts the user with run-time messages whenever an error is encountered in the run of a specification.
In this paper the use of the ASTRAL model checker for cryptographic protocol analysis is presented. The classic benchmarks being investigated include the Needham-Schroeder public-key authentication protocol and the TMN protocol.