Sciweavers

CHARME
2003
Springer

On the Correctness of an Intrusion-Tolerant Group Communication Protocol

14 years 5 months ago
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.
Mohamed Layouni, Jozef Hooman, Sofiène Taha
Added 06 Jul 2010
Updated 06 Jul 2010
Type Conference
Year 2003
Where CHARME
Authors Mohamed Layouni, Jozef Hooman, Sofiène Tahar
Comments (0)