Login | Register

On the formal verification of group key security protocols


On the formal verification of group key security protocols

Gawanmeh, Amjad (2008) On the formal verification of group key security protocols. PhD thesis, Concordia University.

[thumbnail of NR45659.pdf]
Text (application/pdf)
NR45659.pdf - Accepted Version


The correctness of group key security protocols in communication systems remains a great challenge because of dynamic characteristics of group key construction as we deal with an open number of group members. Therefore, verification approaches for two parties protocols cannot be applied on group key protocols. Security properties that are well defined in normal two-party protocols have different meanings and different interpretations in group key distribution protocols, and so they require a more precise definition before we look at how to verify them. An example of such properties is secrecy, which has more complex variations in group key context: forward secrecy, backward secrecy, and key independence. In this thesis, we present a combination of three different theorem-proving methods to verify security properties for group-oriented protocols. We target regular group secrecy, forward secrecy, backward secrecy, and collusion properties for group key protocols. In the first method, rank theorems for forward properties are established based on a set of generic formal specification requirements for group key management and distribution protocols. Rank theorems imply the validity of the security property to be proved, and are deducted from a set of rank functions we define over the protocol. Rank theorems can only reason about absence of attacks in group key protocols. In the second method, a sound and complete inference system is provided to detect attacks in group key management protocols. The inference system provides an elegant and natural proof strategy for such protocols compared to existing approaches. It complements rank theorems by providing a method to reason about the existence of attacks in group key protocols. However, these two methods are based on interactive higher-order logic theorem proving, and therefore require expensive user interactions. Therefore, in the third method, an automation sense is added to the above techniques by using an event-B first-order theorem proving system to provide invariant checking for group key secrecy property and forward secrecy property. This is not a straightforward task, and should be based on a correct semantical link between group key protocols and event-B models. However, in this method, the number of protocol participants that can be considered is limited, it is also applicable on a single protocol event. Finally, it cannot model backward secrecy and key independence. We applied each of the developed methods on a different group protocol from the literature illustrating the features of each approach.

Divisions:Concordia University > Gina Cody School of Engineering and Computer Science > Electrical and Computer Engineering
Item Type:Thesis (PhD)
Authors:Gawanmeh, Amjad
Pagination:xiv, 141 leaves : ill. ; 29 cm.
Institution:Concordia University
Degree Name:Ph. D.
Program:Electrical and Computer Engineering
Thesis Supervisor(s):Tahar, S
Identification Number:LE 3 C66E44P 2008 G39
ID Code:975204
Deposited By: Concordia University Library
Deposited On:22 Jan 2013 15:44
Last Modified:13 Jul 2020 20:07
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