Using model checking to analyze network vulnerabilities

By Ronald W. Ritchey, Paul Ammann. Proceeding 2000 IEEE Symposium on Security and Privacy. S&P 2000, 2000

485 citations recorded by the source corpus.

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

Automated generation and analysis of attack graphs (2002, background): “Following Ritchey and Ammann [20], connectivity is expressed as a ternary relation R E Host x Host x Port, where R(hl, h2,p) means that host h2 is reachable from host hl on port p. Note that the connectivity relation incorporates firewalls and other elements that restrict the ability of one host to ”
Efficient minimum-cost network hardening via exploit dependency graphs (2003, methodology): “On the research front, model checking has been applied to the analysis of single hosts [1] as well as network wide [2].”
Scalable, graph-based network vulnerability analysis (2002, result): “We treat vulnerabilities, attacker access privileges, and network connectivity in a way similar to other authors [13] [12], but with some simplification.”
Model-based evaluation: from dependability to security (2004, background): “, [47], [12]), where the network state includes a description of hosts and their vulnerabilities and a description of connectivity.”
Two formal analyses of attack graphs (2002, methodology): “There are efficient BDD algorithms for all operations used in the algorithm shown in Figure 2.”
An Attack Graph-Based Probabilistic Security Metric (2008, background): “Based on whether a search starts from the initial state or the final state, such analyses can be forward [21,26] or backward [23,24].”