On the Correctness of an Intrusion-Tolerant Group Communication Protocol
Jozef Hooman, and
Proceedings of the 12th Conference on Correct Hardware Design
and Verification Methods (CHARME 2003),
pages 231-246, 2003.
Intrusion-tolerance is the technique of using fault-tolerance to achieve
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
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,
with the title:
Modeling and Verification of Leaders Agreement
in the Intrusion-Tolerant Enclaves Using PVS.