Hardware Verification Group

Concordia University
Text Box: Project Summary: Text Box: Formal Verification of Cryptographic Protocols  Text Box: Publications: Text Box: Conference Papers Text Box: Technical Reports Text Box: Project Members: Text Box: Journal Papers Text Box: Thesis

 

Many of today's distributed applications rely on communication between groups of users. Such applications involve a set of participants that may not fully trust each others. Even if group participants are, a priori, trusted, it is still safe to assume that an external attacker may gain illicit access to the system. Intrusion-tolerance is the application of fault-tolerance to security. Assuming that faults, both benign and Byzantine, are 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 sub-parts.

In this project, we consider the Intrusion-tolerant Enclaves protocol, a Byzantine fault-tolerant platform for secure group communication developed at SRI. We formally analyse the protocol, with a special focus the processes Byzantine behaviour, using an adaptive combination of techniques including Model Checking, Theorem Proving and Analytical mathematics.

 

· M. Layouni, J. Hooman, and S. Tahar: Modeling and Verification of Leaders Agreement in the Intrusion-Tolerant Enclaves Using PVS; B-Track Proc. International Conference on Theorem Proving in Higher-Order Logics (TPHOLs'03), Roma, Italy, September 2003, pp145-158. [In: D. Basin and B. Wolff (Eds.), TPHOLs 2003 Emerging Trends Proceedings, Technical Report No. 187, Institut of Informatics, Albert-Ludwigs University, Freiburg, Germany.]

 

· M. Layouni, J. Hooman, and S. Tahar: On the Correctness of an Intrusion-Tolerant Group Communication Protocol. In the Proceedings of the 12th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME'03), L'Aquila, Italy, October 2003. Springer-Verlag.

 

· M. Layouni, J. Hooman and S. Tahar: Formal Specification and Verification of the Intrusion-Tolerant Enclaves Protocol; Technical Report, Concordia University, Department of Electrical and Computer Engineering, November 2003. [23 pages]

 

· M. Layouni, J. Hooman, and S. Tahar: Modeling and Verification of Leaders Agreement in the Intrusion-Tolerant Enclaves Using PVS; Technical Report, Concordia University, Department of Electrical and Computer Engineering, May 2003. [13 pages].

bullet

Mohamed Layouni

bullet

Dr. Sofiene Tahar

bullet

Dr. Jozef Hooman

 

· M. Layouni, J. Hooman, and S. Tahar: Formal Specification and Verification of the Intrusion-Tolerant Enclaves Protocol; International Journal of Network Security, Vol. 5, No. 3, Science Publications, 2007, pp. 288-298.

 

· Mohamed Layouni, "On the Formal Verification of an Intrusion-Tolerant Group Communications Protocol". M.A.Sc. Thesis, Department of Electrical and Computer Engineering, Concordia University, Montreal, Quebec, Canada, August 2003.