Browse DORAS
Browse Theses
Search
Latest Additions
Creative Commons License
Except where otherwise noted, content on this site is licensed for use under a:

Defining an approximation to formally verify cryptographic protocols

Oehl, Frederic Enoha (2006) Defining an approximation to formally verify cryptographic protocols. Master of Science thesis, Dublin City University.

Full text available as:

[img]PDF - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
4Mb

Abstract

Electronic forms of communication are abundant in todays world, and much emphasis is placed on these methods of communication in every day life. In order to guarantee the secrecy and authenticity of information exchanged, it is vital to formally verify the cryptographic protocols used in these forms of communications. This verification does, however, present many challenges. The systems to verify are infinite, with an infinite number of sessions and of p articipants. As if this was not enough, there is also a reactive element to deal with: th e intruder. The intruder will attack the protocol to achieve his goal: usurping identity, stealing confidential information, etc. His behavior is unpredictable! This thesis describes a method of verification based 011 the verification of systems by approximation. Starting from an initial configuration of the network, an overapproximation of the set of messages exchanged is automatically computed. Secrecy and authentication properties can then be checked on the approximated system. Starting from an existing semi-automatic proof method developed by Genet and Klay, an automatic solution is developed. Starting from an existing semi-automatic proof method developed by Genet and Klay, an automatic solution is developed. This thesis defines a particular approximation function that can be generated automatically and that guarantees that the computation of the approximated system terminates. Th e verification by approximation only tells if properties are verified. When the verification fails no conclusion can be drawn on the property. Thus, this thesis also shows how the approximation technique can easily be combined with another verification technique to combine the strengths of both approaches. Finally, the tool developed to validate these developments and the results of cryptographic protocol verifications carried out in the course of this research are included.

Item Type:Thesis (Master of Science)
Date of Award:2006
Refereed:No
Supervisor(s):SInclair, David
Uncontrolled Keywords:Cryptography; Encryption; Verification systems
Subjects:Computer Science > Computer networks
Computer Science > Computer security
DCU Faculties and Centres:DCU Faculties and Schools > Faculty of Engineering and Computing > School of Computing
Use License:This item is licensed under a Creative Commons Attribution-NonCommercial-No Derivative Works 3.0 License. View License
ID Code:18135
Deposited On:10 May 2013 11:29 by Celine Campbell. Last Modified 10 May 2013 11:29

Download statistics

Archive Staff Only: edit this record