@Article{	  basin.ea:verifying:2007,
  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.},
  author	= {David Basin and Hironobu Kuruma and Kunihiko Miyazaki and
		  Kazuo Takaragi and Burkhart Wolff},
  copyright	= {\copyright Springer-Verlag},
  journal	= {Formal Aspects of Computing},
  language	= {USenglish},
  month		= {March},
  number	= 1,
  pages		= {63--91},
  title		= {Verifying a signature architecture: a comparative case
		  study},
  volume	= 19,
  year		= 2007
}