Abstract:

A Formal Analysis of a Digital Signature Architecture

David Basin and Kunihiko Miyazaki and Kazuo Takaragi


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.