Zhe Dang
Richard A. Kemmerer
Reliable Software Group
Department of Computer Science
University of California
Santa Barbara, CA 93106
ASTRAL is a formal specification language for real-time systems. It is intended to support formal software development, and therefore has been formally defined. This paper focuses on the mechanism of the ASTRAL model checker and how it can be used to analyze encryption protocols.
Key Words: Encryption protocols, Formal methods, Formal specification and verification, Real-time systems, Timing requirements, Proof obligations, State machines, ASTRAL.