An integral part of modeling the global view of network security is
constructing attack graphs. In practice, attack graphs are
produced manually by Red Teams. Construction by hand, however, is
tedious, error-prone, and impractical for attack graphs larger than a
hundred nodes. In this paper we present an automated technique for
generating and analyzing attack graphs. We base our technique on
symbolic model checking algorithms,
letting us construct attack graphs automatically and efficiently. We
also describe two kinds of analysis on attack graphs for helping
analysts decide which attacks would be most cost-effective to guard
against. We implemented our technique in a tool suite and tested it
on a small network example, which includes models of a firewall and
intrusion detection system.
Security and Privacy paper.
Technical report.
Verifiable Secret Sharing
We present a new protocol for verifiably redistributing secrets from
an (m, n) threshold sharing scheme to an (m', n') scheme. Our protocl
guards against dynamic adversaries. We observe that existing
protocols either cannot be readily extended to allow redistribution
between different threshold schemes, or have vulnerabilities that allow faulty old shareholders to distribute invalid shares to new shareholders. Our primary contribution is that in our protocol, new shareholders can verify the validity of their shares after redistribution between different threshold shemes.
Theory Generation
We introduce theory generation, a new general-purpose
technique for performing automated verification. Theory generation
draws inspiration from, and complements, both automated theorem
proving and symbolic model checking, the two approaches that currently
dominate mechanical reasoning. At the core of this approach is the
notion of producing a finite representation of a theory---all the
facts derivable from a set of assumptions. We present an algorithm
for producing compact theory representations for an expressive class
of simple logics.
Security-sensitive protocols are widely used today, and the
growing popularity of electronic commerce is leading to increasing
reliance on them. Though simple in structure, these protocols are
notoriously difficult to design properly. Since specifications of
these protocols typically involve only a small number of principals,
keys, nonces, and messages, and since many properties of interest can
be expressed in ``little logics'' such as the Burrows, Abadi, and
Needham (BAN) logic of authentication, this domain is amenable to
theory generation.
Theory generation enables fast, automated analysis of these
security protocols. Given the theory representation generated from a
protocol specification, one can quickly test for specific desired
properties, as well as directly manipulate the representation to
perform other kinds of analysis, such as protocol comparison. This
paper describes applications of theory generation to more than a dozen
security protocols using four different logics of belief; these
examples confirm, or in some cases expose flaws in earlier analyses.
Updated: 10-Jan-2002
Email Maintainer