On the formal verification of an intrusion-tolerant group communication protocol