Breadcrumb

 
 

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.

[img]
Preview
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 > Faculty 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:Theses (M.A.Sc.)
Program:Electrical and Computer Engineering
Date:2003
Thesis Supervisor(s):Tahar, Sofiene
ID Code:2282
Deposited By:Concordia University Libraries
Deposited On:27 Aug 2009 13:26
Last Modified:08 Dec 2010 10:25
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

Document Downloads

More statistics for this item...

Concordia University - Footer