Formal Modeling and Verification of High-Availability Protocol for Network Security Appliances