@INCOLLECTION{iicis03,
AUTHOR        = {David Basin and Kunihiko Miyazaki and Kazuo Takaragi},
TITLE         = {A Formal Analysis of a Digital Signature Architecture},
BOOKTITLE     = {Integrity and Internal Control in Information Systems, IV},
PUBLISHER     = {Kluwer Academic Publishers},
EDITOR        = {Sushil Jajodia and Leon Strous},
YEAR          = {2004},
PAGES         = {31--48},
BIBTYPE       = {INCOLLECTION},
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.}
}