Login | Register

On the formal verification of an intrusion-tolerant group communication protocol

Title:

On the formal verification of an intrusion-tolerant group communication protocol

Layouni, Mohamed (2003) On the formal verification of an intrusion-tolerant group communication protocol. Masters thesis, Concordia University.

[thumbnail of MQ83868.pdf]
Preview
Text (application/pdf)
MQ83868.pdf
4MB

Abstract

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 > Gina Cody School of Engineering and Computer Science > Electrical and Computer Engineering
Item Type:Thesis (Masters)
Authors:Layouni, Mohamed
Pagination:xi, 97 leaves ; 29 cm.
Institution:Concordia University
Degree Name:M.A. Sc.
Program:Electrical and Computer Engineering
Date:2003
Thesis Supervisor(s):Tahar, Sofiene
Identification Number:QA 76.9 F38L39 2003
ID Code:2282
Deposited By: Concordia University Library
Deposited On:27 Aug 2009 17:26
Last Modified:13 Jul 2020 19:51
Related URLs:
All items in Spectrum are protected by copyright, with all rights reserved. The use of items is governed by Spectrum's terms of access.

Repository Staff Only: item control page

Downloads per month over past year

Research related to the current document (at the CORE website)
- Research related to the current document (at the CORE website)
Back to top Back to top