Please use this identifier to cite or link to this item:
Title: Directed Symbolic Model Checking of Security Protocols
Authors: Nizamani, Qurat Ul Ain
Supervisors: Tuosto, Emilio
Fiadeiro, Jose
Award date: 1-Nov-2011
Presented at: University of Leicester
Abstract: This thesis promotes the use of directed model checking for security protocol verification. In particular, we investigated the possibility of designing heuristics that can reduce the overall size of the state space and can direct the search towards states containing an attack. More precisely, • We have designed three property-specific heuristics namely H1, H2, and H3. The heuristics derive their hints from the security property to be verified and assign weights to states according to their possibility of leading to an attack. • H1 is formally proved correct, i.e., the states pruned by the heuristic H1 do not contain any attack. • An existing tool ASPASyA with conventional model checking algorithm (i.e., depth first search) has been modified so as to integrate our heuristics into it. The resulting tool H -ASPASyA uses an informed search algorithm that is equipped with our heuristics. The heuristics evaluate the states which are then explored in decreasing order of their weights. • The new tool H -ASPASyA is tested against a few protocols to gauge the performance of our heuristics. The results demonstrate the efficiency of our approach. It is worth mentioning that despite being a widely applied verification technique, model checking suffers from the state space explosion problem. Recently directed model checking has been used to mitigate the state space explosion problem in general model checking. However, the directed model checking approaches have not been studied extensively for security protocol verification. This thesis demonstrates the fact that directed model checking can be adapted for security protocol verification in order to yield better results.
Type: Thesis
Level: Doctoral
Qualification: PhD
Rights: Copyright © the author, 2011
Appears in Collections:Theses, Dept. of Computer Science
Leicester Theses

Files in This Item:
File Description SizeFormat 
2011NizamaniQAphd.pdf626.94 kBAdobe PDFView/Open

Items in LRA are protected by copyright, with all rights reserved, unless otherwise indicated.