Login | Register

Formal Specification and Verification of the Intrusion-Tolerant Enclaves Protocol

Title:

Formal Specification and Verification of the Intrusion-Tolerant Enclaves Protocol

Layouni, Mohamed, Hooman, Jozef and Tahar, Sofiène (2007) Formal Specification and Verification of the Intrusion-Tolerant Enclaves Protocol. International Journal of Network Security, 5 (3). pp. 288-298. ISSN 1816-3548

[img]
Preview
Text (application/pdf)
IJNS-2007.pdf - Accepted Version
144kB

Official URL: http://ijns.femto.com.tw/contents/ijns-v5-n3/ijns-...

Abstract

We demonstrate the application of formal methods to the verification of intrusion-tolerant agreement protocols that have a distributed leadership and can tolerate Byzantine faults. As an interesting case study, the Enclaves group-membership protocol has been verified using two techniques: model checking and theorem proving. We use the model checker Murphi to prove the correctness of authentication, and the interactive theorem prover PVS to formally specify and verify Byzantine agreement, termination of agreement, and integrity.

Divisions:Concordia University > Gina Cody School of Engineering and Computer Science > Electrical and Computer Engineering
Item Type:Article
Refereed:Yes
Authors:Layouni, Mohamed and Hooman, Jozef and Tahar, Sofiène
Journal or Publication:International Journal of Network Security
Date:1 November 2007
ID Code:977374
Deposited By: DANIELLE DENNIE
Deposited On:14 Jun 2013 15:05
Last Modified:18 Jan 2018 17:44
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

Back to top Back to top