On the correctness of an intrusion-tolerant group communication protocol

Intrusion-tolerance is the technique of using fault-tolerance to achieve security properties. Assuming that faults, both benign and Byzantine, are unavoidable, the main goal of Intrusion-tolerance is to preserve an acceptable, though possibly degraded, service of the overall system despite intrusions at some of its sub-parts. In this paper, we present a correctness proof of the Intrusion-tolerant Enclaves protocol [1] via an adaptive combination of techniques, namely model checking, theorem proving and analytical mathematics. We use Murphi to verify authentication, then PVS to formally specify and prove proper Byzantine Agreement, Agreement Termination and Integrity, and finally we mathematically prove robustness of the group key management module.