Open access
Date
2005Type
- Report
ETH Bibliography
yes
Altmetrics
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). Show more
Permanent link
https://doi.org/10.3929/ethz-a-006775722Publication status
publishedJournal / series
Technical reportVolume
Publisher
ETHSubject
SPEZIFIKATIONEN (SOFTWARE ENGINEERING); VERIFICATION (SOFTWARE ENGINEERING); VERIFIKATION (SOFTWARE ENGINEERING); SPECIFICATIONS (SOFTWARE ENGINEERING); DIGITAL SIGNATURES (INFORMATION THEORY); DIGITALE SIGNATUREN (INFORMATIONSTHEORIE)Organisational unit
02150 - Dep. Informatik / Dep. of Computer Science03634 - Basin, David / Basin, David
More
Show all metadata
ETH Bibliography
yes
Altmetrics