English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
 
 
DownloadE-Mail
 Local TagsRelease HistoryDetailsSummary
  Formalization and Verification of Informal Security Protocol Description

Kiraz, M. S. (2003). Formalization and Verification of Informal Security Protocol Description. Master Thesis, Universität des Saarlandes, Saarbrücken.

Item is

 

show all hide all

Basic

show hide
Item Permalink: https://hdl.handle.net/11858/00-001M-0000-0027-F819-B Version Permalink: https://hdl.handle.net/11858/00-001M-0000-0027-F81A-9
Genre: Thesis

Files

show Files

Locators

show

Creators

show
hide
 Creators:
Kiraz, Mehmet Sabir1, Author
Blanchet, Bruno2, Advisor           
Affiliations:
1International Max Planck Research School, MPI for Informatics, Max Planck Society, Campus E1 4, 66123 Saarbrücken, DE, ou_1116551              
2Static Analysis, MPI for Informatics, Max Planck Society, ou_1116553              

Content

show
hide
Free keywords: -
 Abstract: Conclusions: In this master thesis, we have started with an informal security protocol representation. We have demonstrated the translation of protocols into Horn clauses by giving the well-known Otway Rees Protocol as an example. We also defined and formalized semantics of the protocol for all participant. For the work presented in this thesis we have assumed perfect encryption. We also assume that the protocol is executed in the presence of the attacker that can listen, compute new messages from the messages it has already received, and send any message it can build. We firmalized the abilities of attacker and we defined the view of attacker to the message. By looking to the view of the messages, if participant can distiguish the views then it will stop the protocol run, if participant cannot distinguish the messages from each other then it will reply to the previous message. The related work has been done in the reference [5] for CAPSL ( Common Authentication Protocol Specification Language) wich is a high-level language for applying formal methods to the security analysis of cryptographic protocols. Protocol is specified in a form that could be used as the input format for any formal analysis.

Details

show
hide
Language(s): eng - English
 Dates: 20032003
 Publication Status: Issued
 Pages: -
 Publishing info: Saarbrücken : Universität des Saarlandes
 Table of Contents: -
 Rev. Type: -
 Identifiers: BibTex Citekey: Kiraz2003
 Degree: Master

Event

show

Legal Case

show

Project information

show

Source

show