One of the prerequisites for information society is secure and reliable communication among computing systems. Thus, for both fault tolerance and high network throughput, multiple security appliances are often deployed together in a group. In this paper, we present our expe- rience of formally modeling and verifying a group management protocol for network security appliances using the Spin model checker. To analyze the reliability of the protocol, we classified and modeled various types of faults and analyzed the protocol in the presence of combination of these faults.