On the Correctness of an Intrusion-Tolerant Group Communication Protocol

Mohamed Layouni, Jozef Hooman, and Sofične Tahar

Appeared in: Proceedings of the 12th Conference on Correct Hardware Design and Verification Methods (CHARME 2003), LNCS 2860, Springer-Verlag, pages 231-246, 2003.

ABSTRACT

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 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.

Paper (postscript) © Springer-Verlag -      PVS dump file with all theories and proofs

A preliminary version appeared as Technical Report of the Department of Electrical and Computer Engineering, Concordia University, Montreal, Canada, with the title: Modeling and Verification of Leaders Agreement in the Intrusion-Tolerant Enclaves Using PVS.