Verification of Security Properties Using Formal Techniques

von Saleh Al-Shadly
Dissertation
Datum der mündl. Prüfung:2013-04-09
Erschienen:2014-02-12
Betreuer:Prof. Dr. Dieter Hogrefe
Gutachter:Prof. Dr. Dieter Hogrefe
Gutachter:Prof. Dr. Xiaoming Fu
Gutachter:Prof. Dr. Jens Grabowski
Gutachter:Prof. Dr. Modrow Eckart
Gutachter:Prof. Dr. Konrad Rieck
Gutachter:Prof. Dr. Stephan Waack
Zum Verlinken/Zitieren: http://dx.doi.org/10.53846/goediss-4357

 

 

Dateien

Name:Thesis-SA.pdf
Size:1.21Mb
Format:PDF
Description:PhD Thesis

Lizenzbestimmungen:

Zusammenfassung

Englisch

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
 
Statistik