Verification of Security Properties Using Formal Techniques
by Saleh Al-Shadly
Date of Examination:2013-04-09
Date of issue:2014-02-12
Advisor:Prof. Dr. Dieter Hogrefe
Referee:Prof. Dr. Dieter Hogrefe
Referee:Prof. Dr. Xiaoming Fu
Referee:Prof. Dr. Jens Grabowski
Referee:Prof. Dr. Modrow Eckart
Referee:Prof. Dr. Konrad Rieck
Referee:Prof. Dr. Stephan Waack
Files in this item
Name:Thesis-SA.pdf
Size:1.21Mb
Format:PDF
Description:PhD Thesis
Abstract
English
Nowadays, the necessity of developing collaborative and distributed computing systems makes networks, and specially Internet, the key element of the system design process. Several new applications have been appeared in the Internet which require a variety of security requirements must be ful lled. There are applications that exchange sensitive and private information which must be secret and authentic. Other applications (i.e. real-time applications) which require a certain level of quality of service should be maintained. Thus, the traditional solutions can not ful ll the new requirements. Usually, requirements such as con dentiality and integrity are provided using cryptography. In current computing systems, cryptography should not only provide those requirements but also it must guarantee other security requirements such as non-repudiation, anonymity, DoS-resistance, and so on. Consequently, new security protocols must be proposed in order to cover the continuous needs. Due to distributed nature of security protocols and the hostile environment where they are usually executed, the design of correct security protocols is di cult and error-prone. Thus, analyzing their correctness is a crucial task. Formal methods have been intensively used for analyzing con dentiality and integrity requirements and there exists several automated tools for such analysis. However, the use of formal methods for analyzing requirements such as DoS-resistance is still not mature and an emergent eld. This research is concerned to study the application of formal techniques in speci cation and veri cation of security requirements focusing on authentication, secrecy and DoS-resistance requirements. Additionally, an attempt to quantify the impact of denial of service attacks on the network and evaluate their defense mechanisms is also presented. Speci c outcomes of this work include: A comprehensive survey of most important formal techniques and tools for speci cation and veri cation of security protocols; Analysis of authentication and secrecy requirements of an authentication protocol of inter-domain handover using AVISPA toolkit; Presenting the state-of-art of formal techniques of denial of modeling and analysis of service as well as other DoS basic knowledge such as types of DoS attacks, attack tools, defense mechanisms and strategies, etc; Quantifying the impact of DoS attacks on networks and evaluating their active defenses through simulation, and Outlook for automating Meadows's cost-based framework using probabilistic model checking.
Keywords: Model checking; Security protocols; Security properties; Formal methods; Formal techniques