Scenario and Attack Graphs
Contents
Introduction
Model checking is a technique for determining whether a formal
model of a system satisfies a given property. If the property is
false in the model, model checkers typically produce a single
counterexample. The developer uses this counterexample to revise the
model (or the property), which often means fixing a bug in the design
of the system. The developer then iterates through the process,
rechecking the revised model against the (possibly revised)
property.
Sometimes, however, we would like all counterexamples, not
just one. Rather than produce one example of how the model does not
satisfy a given property, why not produce all of them at once? We
call the set of all counterexamples a scenario graph. For a
traditional use of model checking, e.g., to find bugs, each path in
the graph represents a counterexample, i.e., a failure scenario. In
our application to security, each path represents an attack, a way in
which an intruder can attack a system. Attack graphs are a special
case of scenario graphs.
Attack graphs depict ways in which an adversary can
exploit vulnerabilities to break into a system. System administrators
analyze attack graphs to understand where their system's weaknesses
lie and to help decide which security measures will be effective to
deploy. In practice, attack graphs are produced manually by Red
Teams. Construction by hand, however, is tedious, errorprone, and
impractical for attack graphs larger than a hundred nodes.
Our attack graph toolkit generates scenario graphs from a network
attack model and a security property. An example security property is
that an intruder should never gain root access to a specific host.
Since each scenario graph is propertyspecific, in practice, we might
need to generate many scenario graphs to represent the entire attack
graph that a Red Team might construct manually. Our main advantage is
that we automate the process of producing scenario graphs.
People
Current
Past
 Oleg Sheyner
 Oren Dobzinski
 Yanjing Li
 Meera Sridhar
 Arvind Kannan
 Roman V. Lototski
 Alexey Roschyna
Publications

Jeannette M. Wing.
Scenario graphs applied to security.
To appear in David Tipper, Prashant Krishnamurthy, Yi Quian, and James Joshi, editors, Information Assurance: Survivability and Security in Networked Systems, Morgan Kaufmann Publishers, Elsevier, Inc., draft submitted December 2006.

Vaibhav Mehta, Constantinos Bartzis, Haifeng Zhu, Edmund Clarke, and Jeannette Wing.
Ranking attack graphs.
In Diego Zamboni and Christopher Kruegel, editors, Proceedings of the 9th International Symposium on Recent Advances in Intrusion Detection, Hamburg, Germany, September 2006.
Springer LNCS 4219.

Jeannette M. Wing.
Scenario graphs applied to security.
In Edmund M. Clarke, Marius Minea, and Ferucio Laurentiu Tiplea, editors, Proceedings of the NATO Workshop on Verification of Infinite State Systems with Applications to Security, Timisoara, Romania, March 2005.
Summary paper.

Oleg Mikhail Sheyner.
Scenario Graphs and Attack Graphs.
PhD thesis, School of Computer Science, Carnegie Mellon University, April 2004.

Oleg Sheyner and Jeannette Wing.
Tools for generating and analyzing attack graphs.
In Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, and WillemPaul de Roever, editors, Proceedings of the Second International Symposium on Formal Methods for Components and Objects, Leiden, The Netherlands, November 2003.
Springer LNCS 3188.

S. Jha, O. Sheyner, and J. Wing.
Two formal analyses of attack graphs.
In Proceedings of the 15th IEEE Computer Security Foundations Workshop, Nova Scotia, Canada, June 2002.

Oleg Sheyner, Joshua Haines, Somesh Jha, Richard Lippmann, and Jeannette M. Wing.
Automated generation and analysis of attack graphs.
In Proceedings of the 2002 IEEE Symposium on Security and Privacy, Oakland, CA, May 2002.

Somesh Jha and Jeannette M. Wing.
Survivability analysis of networked systems.
In Proceedings of the International Conference on Software Engineering, Toronto, Canada, May 2001.
Preliminary version available as CMUCS00168, October 2000.

S. Jha, J. Wing, R. Linger, and T. Longstaff.
Survivability analysis of network specifications.
In Proceedings of the International Conference on Dependable Systems and Networks, Workshop on Dependability Despite Maliciowns FauIts, New York, NY, June 2000.
Software
The current release of the attack graph toolkit is version 20070201.
 attackgraph20070201.tar.gz
 The code has been reorganized and made to work with recent C/C++ compilers.
 attackgraph20051121.tar.gz (obsolete)
 The original release of the attack graph toolkit, developed by Oleg Sheyner, Roman Lototski, Alexey Roschyna, and others.