Abstract:

Verification of a Signature Architecture with HOL-Z

David Basin and Hironobu Kuruma and Kazuo Takaragi and Burkhart Wolff


We report on a case study in using HOL-Z, an embedding of Z in higher-order logic, to 
specify and verify a security architecture for administering digital signatures. We have 
used HOL-Z to formalize and combine both data-oriented and process-oriented architectural 
views. Afterwards, we formalized temporal requirements in Z and carried out verification 
in higher-order logic. The same architecture has been previously verified using the SPIN 
model checker. Based on this, 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 rich 
data. Moreover, our comparison highlights the advantages of this approach and provides 
evidence that, in the hands of experienced users, theorem proving is neither substantially 
ore time-consuming nor more complex than model checking.