@TechReport{	  basin.ea:specifying:2005,
  abstract	= {We report on a case-study in using the data-oriented
		  modeling language Z to formalize a security architecture
		  for administering digital signatures and its architectural
		  security requirements. Within an embedding of Z in the
		  higher-order logic Isabelle/HOL, we provide formal
		  machine-checked proofs of the correctness of the
		  architecture with respect to its requirements. A
		  formalization and verification of the same architecture has
		  been previously carried out using the process-oriented
		  modeling language PROMELA and the SPIN model checker. We
		  use this as a basis for comparing these two different
		  approaches to formalization (infinite state with rich data
		  types versus finite state) and verification (theorem
		  proving versus model checking).},
  author	= {David Basin and Hironobu Kuruma and Kazuo Takaragi and
		  Burkhart Wolff},
  institution	= {Computer Security Group, ETH Z\"urich},
  language	= {USenglish},
  month		= 1,
  number	= 471,
  pdf		= {papers/2005/HSD.pdf},
  title		= {Specifying and Verifying Hysteresis Signature System with
		  HOL-Z},
  year		= 2005,
  user		= {wolff}
}