非表示:
キーワード:
-
要旨:
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.
