Since the correctness of a firewall configuration is the focus of this book, we assume a firewall is correct iff (if and only if) its configuration is correct, and a firewall configuration is correct iff it satisfies its given requirement specification, which is usually written in a natural language. In the rest of this book, we use “firewall” to mean “firewall configuration” if not otherwise specified. In this book, for ease of presentation, we assume that a firewall maps every packet to one of two decisions: accept or discard. Most firewall software supports more than two decisions such as accept, accept-and-log, discard, and discard-and-log. Our firewall design and analysis methods can be straightforwardly extended to support more than two decisions. The firewall design and analysis methods presented in this book are not limited to just firewalls. Rather, they are extensible to other rulePrologue