Sciweavers

FAC
2007

Verifying a signature architecture: a comparative case study

13 years 10 months ago
Verifying a signature architecture: a comparative case study
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, which we verify by finite-state model checking. We provide a detailed comparison of the...
David A. Basin, Hironobu Kuruma, Kunihiko Miyazaki
Added 14 Dec 2010
Updated 14 Dec 2010
Type Journal
Year 2007
Where FAC
Authors David A. Basin, Hironobu Kuruma, Kunihiko Miyazaki, Kazuo Takaragi, Burkhart Wolff
Comments (0)