Information Assurance

Acknowledgments

Oleg Sheyner deserves all the credit for the technical contributions summarized in this chapter. The initial idea of using model checking to produce attack graphs is due to my collaboration with Somesh Jha.

All the ideas in this chapter can be found in greater detail in Oleg Sheyner’s doctoral dissertation [3]. Portions of his dissertation have appeared in conference and journal papers [1, 2, 5, 13, 16, 29]. This chapter draws largely from Wing’s summary paper [29] and Sheyner and Wing’s conference paper [16]; specific sections are reprinted in part from Wing [29], pp. 229–234, with permission from IOS Press, and Sheyner and Wing [16], pp. 344–371, Figures 2–7, with kind permission of Springer Science and Business Media.

This ...