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: layouni@ece.concordia.ca