Abstract
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 more time-consuming nor more complex than model checking.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Abrial, J.-R.: The B-book: assigning programs to meanings. Cambridge University Press, Cambridge (1996)
Arai, T., Sekiguchi, T., Satoh, M., Inoue, T., Nakamura, T., Iwao, H.: Darma: Using different OSs concurrently based on nano-kernel technology. In: Proc. 59th-Annual Convention of Information Processing Society of Japan. Information Processing Society of Japan, vol. 1, pp. 139–140 (1999) (in Japanese)
Basin, D., Kaufmann, M.: The Boyer-Moore Prover and Nuprl: An experimental comparison. In: Huet, G., Plotkin, G. (eds.) Logical Frameworks, pp. 90–119. Cambridge University Press, Cambridge (1991)
Basin, D., Kuruma, H., Takaragi, K., Wolff, B.: Specifying and verifying hysteresis signature system with HOL-Z. Technical Report 471, ETH Zürich (January 2004), http://kisogawa.inf.ethz.ch/WebBIB/publications/papers/2005/HSD.pdf
Basin, D., Miyazaki, K., Takaragi, K.: A formal analysis of a digital signature architecture. In: Jajodia, S., Strous, L. (eds.) Integrity and Internal Control in Information Systems, IV, pp. 31–48. Kluwer Academic Publishers, Dordrecht (2004)
Brucker, A.D., Rittinger, F., Wolff, B.: HOL-Z 2.0: A proof environment for Z-specifications. Journal of Universal Computer Science 9(2), 152–172 (2003)
Brucker, A.D., Wolff, B.: A case study of a formalized security architecture. Electronic Notes in Theoretical Computer Science, vol. 80. Elsevier Science Publishers, Amsterdam (2003)
Fischer, C.: CSP-OZ: A combination of Object-Z and CSP. In: Proceedings of FMOODS 1997. Formal Methods for Open Object-Based Distributed Systems, vol. 2, pp. 423–438. Chapman & Hall, Boca Raton (1997)
Gupta, A.: Formal hardware verification methods: A survey. Journal of Formal Methods in System Design 1, 151–238 (1992)
Holzmann, G.J.: The model checker SPIN. Software Engineering 23(5), 279–295 (1997)
International Standard ISO/IEC 13568:2002. Information technology –Z formal specification notation —syntax, type system and semantics
Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)
Smith, G., Derrick, J.: Refinement and verification of concurrent systems specified in Object-Z and CSP. In: Proceedings of the International Conference of Formal Engineering Methods, pp. 293–302. IEEE Computer Society Press, Los Alamitos (1997)
Spivey, J.M.: The Z Notation: A Reference Manual, 2nd edn. Prentice-Hall International, New Jersey (1992)
Susaki, S., Matsumoto, T.: Alibi establishment for electronic signatures. Information Processing Society of Japan 43(8), 2381–2393 (2002) (in Japanese)
Woodcock, J., Davies, J.: Using Z. Prentice-Hall International, New Jersey (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Basin, D., Kuruma, H., Takaragi, K., Wolff, B. (2005). Verification of a Signature Architecture with HOL-Z. In: Fitzgerald, J., Hayes, I.J., Tarlecki, A. (eds) FM 2005: Formal Methods. FM 2005. Lecture Notes in Computer Science, vol 3582. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11526841_19
Download citation
DOI: https://doi.org/10.1007/11526841_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-27882-5
Online ISBN: 978-3-540-31714-2
eBook Packages: Computer ScienceComputer Science (R0)