One of the prerequisites for information society is secure and reliable communication among computing systems. Accordingly, network security appliances become key components of infrastructure, not only as security guardians, but also as reliable network components. Thus, for both fault tolerance and high network throughput, multiple security ap- pliances are often deployed together in a group. In this paper, we present our experience 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 combina- tion of these faults. We could detect several design flaws of the protocol through this project.