Skip to main content
Open Access Publications from the University of California

UC Davis

UC Davis Previously Published Works bannerUC Davis

A Comprehensive Framework for Using Iterative Analysis to Improve Human-Intensive Process Security: An Election Example


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.

Many UC-authored scholarly publications are freely available on this site because of the UC's open access policies. Let us know how this access is important for you.

Main Content
For improved accessibility of PDF content, download the file to your device.
Current View