next up previous
Next: Introduction

Using the ASTRAL Model Checker
for Cryptographic Protocol Analysis

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.