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.