The individual vulnerabilities of hosts on a network can be combined by an attacker to gain access that would not be possible if the hosts were not interconnected. Currently available tools report vulnerabilities in isolation and in the context of individual hosts in a network. Topological vulnerability analysis (TVA) extends this by searching for sequences of interdependent vulnerabilities, distributed among the various network hosts. Model checking has been applied to the analysis of this problem with some interesting initial result. However previous efforts did not take into account a realistic representation of network connectivity. These models were enough to demonstrate the usefulness of the model checking approach but would not be sufficient to analyze real-world network security problems. This paper presents a modem of network connectivity at multiple levels of the TCP/IP stack appropri-ate for use in a model checker. With this enhancement, it is possible to represent realistic networks including common network security devices such as firewalls, filtering routers, and switches.