Firewalls offer a protection for private networks against both internal and external attacks. However, configuring firewalls to ensure the protections is a difficult task. The main reason is the lack of methodology to analyze the security of firewall configurations. IP spoofing attack is an attack in which an attacker can impersonate another person towards a victim. In this paper, we propose a new methodology for verifying the vulnerability of firewall configurations to IP spoofing attack and for synthesizing IP spoofing-free configurations. Our methodology is based on graph theory which provides a simple and intuitive approach to the vulnerability analysis of the attack.