| Intrusion-tolerance is the technique of using fault-tolerance to achieve security properties. Assuming faults to be 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 parts. In this thesis, we are concerned with the formal specification and verification of the Enclaves protocol: an intrusion-tolerant platform for secure group communication. We formally specify the three modules of Enclaves, namely, Authentication, Leaders Agreement and Group Key Management. Then we derive a correctness proof for the whole protocol using an adaptive combination of techniques, namely, model checking, theorem proving and mathematical analysis. We use the Murphi model checking tool to verify authentication, then the PVS theorem prover to formally specify and prove proper Byzantine agreement, agreement termination and integrity, and finally we analytically prove robustness and unpredictability of the Group Key Management module. |
