Layouni, Mohamed (2003) On the formal verification of an intrusion-tolerant group communication protocol. Masters thesis, Concordia University.
Intrusion-tolerance is the technique of using fault-tolerance to achieve security properties. Assuming faults to be 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 parts. In this thesis, we are concerned with the formal specification and verification of the Enclaves protocol: an intrusion-tolerant platform for secure group communication. We formally specify the three modules of Enclaves, namely, Authentication, Leaders Agreement and Group Key Management. Then we derive a correctness proof for the whole protocol using an adaptive combination of techniques, namely, model checking, theorem proving and mathematical analysis. We use the Murphi model checking tool to verify authentication , then the PVS theorem prover to formally specify and prove proper Byzantine agreement , agreement termination and integrity , and finally we analytically prove robustness and unpredictability of the Group Key Management module.
|Divisions:||Concordia University > Faculty of Engineering and Computer Science > Electrical and Computer Engineering|
|Item Type:||Thesis (Masters)|
|Pagination:||xi, 97 leaves ; 29 cm.|
|Degree Name:||Theses (M.A.Sc.)|
|Program:||Electrical and Computer Engineering|
|Thesis Supervisor(s):||Tahar, Sofiene|
|Deposited By:||Concordia University Libraries|
|Deposited On:||27 Aug 2009 17:26|
|Last Modified:||08 Dec 2010 15:25|
Repository Staff Only: item control page