This paper described a methodology to perform procedural security analysis based on explicit reasoning on asset flows -- notably, by building a model to describe the nominal procedures under analysis and, injecting possible threat actions (by assuming that any combination of threats can be possible in all steps) into the model. We also outlined encoding strategies using NuSMV input language --that it is amenable for formal analysis allowing to reason on different properties about the procedure on the extended model such as, the "actor-play-role" principle and "reachability" of (un)desired state of an asset.
Among the advantages, a structured approach to analyze security of procedures and a general threat injection strategy that allows a high level of generality in defining the attacks. The usage of model-checkers, moreover, allows for reasoning about threat composition and to highlight, e.g. the level of coordination and resources required to carry out certain attacks.
The work presented in this paper is on-going. Among the areas of development we mention automation (e.g. algorithms to automatically perform threat injection) and better tool support. Another area of interest relates to provide guidelines that can be incorporated in the Common Criteria [27], both methodologically and tool supported way to automate the analysis.
komminist 2008-06-30
