Formal Specification and Verification of
the Intrusion-Tolerant Enclaves Protocol
Mohamed Layouni, Jozef Hooman, and Sofiene Tahar
International Journal of Network Security
Volume 5, Number 3, pages 288-298, 2007.
ABSTRACT
We demonstrate the application of formal methods to the verification
of intrusion-tolerant agreement protocols that have a distributed
leadership and can tolerate Byzantine faults. As an interesting case
study, the Enclaves group-membership protocol has been verified
using two techniques: model checking and theorem proving. We use the
model checker Murphi to prove the correctness of authentication, and
the interactive theorem prover PVS to formally specify and verify
Byzantine agreement, termination of agreement, and integrity.
pdf of journal
-
local pdf copy