| In this paper, we present a correctness proof of the
Intrusion-tolerant
Enclaves protocol. Enclaves is a group-membership protocol. It assumes a
Byzantine failure model, and has a maximum resiliency of one third. To carry
out the proof, we adaptively combine a number of techniques, namely model
checking, theorem proving and analytical mathematics. We use the
Murphi model checker to verify authentication, then the PVS theorem prover a
Byzantine failure model, and has a maximum resiliency of one third. To carry
out the proof, we adaptively combine a number of techniques, namely model
checking, theorem proving and analytical mathematics. We use the
Murphi model checker to verify authentication, then the PVS theorem prover
to formally specify and prove proper Byzantine Agreement, Agreement
Termination and Integrity, and finally we mathematically prove the
robustness and unpredictability of the group key management module using the
random oracle model. |
Download PDF file (PDF File)