Formal Description and Verification of Security Filtered Rules

With the ever-changing threat of network, packet-filtering firewall, an important instrument for resisting threat, has become the effective measure of host-computer protection. Its ability depends on the capability of filtered rules. This paper first describes filtered rules formally, and then tests the rules including the verification of special aims and security analysis based on model checking. The formal analysis and verification make the rules achieve the security administrators´ will of packet filtering and protect the system safe.