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

fYear

1999

fDate

22-22 May 1999

Firstpage

132

Lastpage

141

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Software Engineering, 1999. Proceedings of the 1999 International Conference on

Conference_Location

Los Angeles, CA, USA

ISSN

0270-5257

Print_ISBN

1-58113-074-0

Type

conf

Filename

841002