Rights / licenseIn Copyright - Non-Commercial Use Permitted
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) Show more
Journal / seriesTechnical report
SubjectSPEZIFIKATIONEN (SOFTWARE ENGINEERING); VERIFICATION (SOFTWARE ENGINEERING); VERIFIKATION (SOFTWARE ENGINEERING); SPECIFICATIONS (SOFTWARE ENGINEERING); DIGITAL SIGNATURES (INFORMATION THEORY); DIGITALE SIGNATUREN (INFORMATIONSTHEORIE)
Organisational unit02150 - Departement Informatik / Department of Computer Science
03634 - Basin, David
NotesTechnical Reports D-INFK.
Technical Reports D-INFK.
Weitere Autoren: Hironobu Kuruma, Kazuo Takaragi, Burkhart Wolff.
MoreShow all metadata