Title :
Using the ASTRAL model checker to analyze Mobile IP
Author :
Dang, Zhe ; Kemmerer, Richard A.
Author_Institution :
Dept. of Comput. Sci., California Univ., Santa Barbara, CA, USA
Abstract :
ASTRAL is a high level formal specification language for real time systems. It is provided with structuring mechanisms that allow one to build modularized specifications of complex real time systems with layering. The ASTRAL model checker checks the satisfiability of critical requirements of a specification by enumerating possible runs of transitions within a given time bound. The paper discusses the mechanism of the model checker and how it can be used to analyze encryption protocols. Several classic benchmarks have been investigated, including the Needham-Schroeder public-key authentication protocol (R.M. Needham and M.D. Schroeder, 1978) and the TMN protocol, and a number of attacks were uncovered. The paper focuses on using ASTRAL to specify Mobile IP (C. Perkins, 1996) and testing the specification using the model checker.
Keywords :
Internet; computability; formal specification; message authentication; mobile computing; program verification; protocols; public key cryptography; real-time systems; specification languages; ASTRAL model checker; Needham-Schroeder public-key authentication protocol; TMN protocol; critical requirements; encryption protocols; high level formal specification language; layering; mobile IP analysis; modularized specifications; real time systems; satisfiability; structuring mechanisms; time bound; Cryptographic protocols; Cryptography; Formal specifications; Mobile computing; Permission; Prototypes; Public key; Real time systems; Specification languages; Testing;
Conference_Titel :
Software Engineering, 1999. Proceedings of the 1999 International Conference on
Conference_Location :
Los Angeles, CA, USA
Print_ISBN :
1-58113-074-0
