To facilitate the development of stateful firewalls, in [Gouda and Liu (2005)], we present a simple model for specifying stateful firewalls. Our model of stateful firewalls has several favorable properties. First, despite its Prologue 7 simplicity, it can express a variety of state tracking functionalities. Second, it allows us to inherit the rich results in stateless firewall design and analysis. Third, it provides backward compatibility such that a stateless firewall can also be specified using our model. Moreover, we present several methods in [Gouda and Liu (2005)] to analyze the properties of a stateful firewall specified in this model.