Verifying a signature architecture: a comparative case study |
| |
Authors: | David Basin Hironobu Kuruma Kunihiko Miyazaki Kazuo Takaragi Burkhart Wolff |
| |
Affiliation: | (1) ETH Zürich, IFW C 49.1, 8092 Zürich, Switzerland;(2) Hitachi, Ltd., Systems Development Laboratory, Kawasaki, Japan;(3) ETH Zürich, IFW C 46.1, 8092 Zürich, Switzerland |
| |
Abstract: | We report on a case study in applying different formal methods to model and verify an architecture for administrating digital
signatures. The architecture comprises several concurrently executing systems that authenticate users and generate and store
digital signatures by passing security relevant data through a tightly controlled interface. The architecture is interesting
from a formal-methods perspective as it involves complex operations on data as well as process coordination and hence is a
candidate for both data-oriented and process-oriented formal methods.
We have built and verified two models of the signature architecture using two representative formal methods. In the first,
we specify a data model of the architecture in Z that we extend to a trace model and interactively verify by theorem proving.
In the second, we model the architecture as a system of communicating processes that we verify by finite-state model checking.
We provide a detailed comparison of these two different approaches to formalization (infinite state with rich data types versus
finite state) and verification (theorem proving versus model checking). Contrary to common belief, our case study suggests
that Z is well suited for temporal reasoning about process models with complex operations on data. Moreover, our comparison
highlights the advantages of proving theorems about such models and provides evidence that, in the hands of an experienced
user, theorem proving may be neither substantially more time-consuming nor more complex than model checking. |
| |
Keywords: | Formal methods Comparison Theorem proving Model checking Security Case study |
本文献已被 SpringerLink 等数据库收录! |
|