David Basin, Hironobu Kuruma, Kunihiko Miyazaki, Kazuo Takaragi, Burkhart Wolff
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...
Verification of a signature architecture with HOL-Z (2005)
David Basin, Hironobu Kuruma, Kazuo Takaragi, Burkhart Wolff
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...