@InCollection{ basin.ea:a-formal-analysis-of-a-digital-signature-architecture:2004, abstract = {{ We report on a case study in applying formal methods to model and validate an architecture for administrating digital signatures. We use a process-oriented modeling language to model a signature system implemented on top of a secure operating system. Afterwards, we use the Spin model checker to validate access control and integrity properties. We describe here our modeling approach and the benefits gained from our analysis.}}, author = {David Basin and Kunihiko Miyazaki and Kazuo Takaragi}, booktitle = {Integrity and Internal Control in Information Systems, IV}, copyright = {Kluwer Academic Publishers}, copyrighturl = {http://www.wkap.nl/copyright}, editor = {{Sushil Jajodia and Leon Strous}}, language = {USenglish}, pages = {31--48}, publisher = {{Kluwer Academic Publishers}}, title = {{A Formal Analysis of a Digital Signature Architecture}}, year = 2004, user = {bgeiser} }