Enclaves is a group-oriented intrusion-tolerant protocol. Intrusion-tolerant
protocols are cryptographic protocols that implement fault-tolerance techniques
to achieve security despite possible intrusions at some parts of the system.
Among the most tedious faults to handle in security are the so-called Byzantine
faults, where insiders maliciously exhibit an arbitrary (possibly dishonest)
behavior during executions of the protocol. This class of faults poses
formidable challenges to current verification techniques and has been formally
verified only in simplified forms and under restricted fault assumptions.
In this paper we present our work on the formal verification of the Byzantine
fault-tolerant Enclaves protocol. We use PVS to formally specify and prove
Proper Byzantine Agreement, Agreement Termination and Integrity.
|Download Postscript file (PS File)|
|Download PDF file (PDF File)|
|Download PVS Theories and Proofs.|
|Download Murphi Specification.|
|Send comments and suggestions to: firstname.lastname@example.org|