Item

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.