UC Davis

This paper presents an approach for analyzing complex processes, including those involving human agents, hardware devices, and software systems, and illustrates the utility of this approach by analyzing part of a process for holding an election. In the work described here, the Little-JIL process definition language is used to create a precise and detailed model of an election process. Given this process definition, two forms of automated analysis are used to explore the possibility that specified security policies could be undermined. Model checking is first used to identify process execution sequences that violate event-sequence security policies and other properties. After these are addressed, fault-tree analysis is applied to identify when the misperformance of steps might allow security breaches or other undesirable outcomes to occur. The results of these analyses can provide assurance about the process, suggest areas for improvement, and, when applied to a modified process definition, evaluate proposed changes in the process.