英语论文网

留学生计算机科学论文 Abstract - Formal method has been advocated as an important means of improving the safety and reliability of software systems, especial those which are safety-critical. We propose a new simple trace semantics that can be used to specify security properties. Our technique support a protocol designer to provide formal Analysis of the security properties. We illustrate the utility of our technique by exposing two attacks on the well studied protocol TMN.

Keywords - Cryptographic Protocols, Formal method, Trace Semantics, Model Checking, SPIN／Promela

Ⅰ.INTRODUCTION
Security protocol is to apply the cryptography to hide means or access to information, with the purpose to certificate message as well as the accurate transmission of the message in networks. At the same time security protocol also for resolving the other network security attributes one of the most effective means. For example, the completion of the sources of information and objectives of the certification; ensure the integrity of the information; distribution of key safety and ensure the security of communications session; notarization and timely to ensure the effectiveness of network communications and so on.

Therefore, security protocol works as a key component of communication and network security systems, as well as the major tools of distributed systems and e-commerce system. As a result,it is quite practical to do some research into cryptographic protocols.

There is a complex interaction of relations and constraints between those cryptographic protocol information, but most of which operate in a complex distributed network environment, what’s more,network involves multi- participants, large-scale operation and dynamic features. To design security protocols , it is inevitable there will be security flaws. Practice has proved that there areserious security flaws in the cryptographic protocol after years of use. For example, it was 17 years later when lowe found the security flaws ofter famous Needham-Schroeder ventilate the cipher code [1].

In this paper the author proposes a new trace semantics, for special security properties and tests the security of cryptographical protocol through model detector SPIN[2, 3] . This experiment proved the effectiveness and versatility, can be easily used for other network security protocol verification. In this paper, as follows: Section II on traces semantics of the Statute of formal protocols; detector SPIN model and its modeling language Promela [2] mechanism set out in the third quarter; fourth quarter to protocol TMN[4] as an example to illustrate the above methods, effectiveness conclusions are given in Section V.

ReferenceS
[1].G. Lowe, “Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR”, Proc. TACAS, LNCS 1055, 147-166, 1996, Springer Verlag.
[2]. G.J.Holzmann, “The SPIN Model Checker, Primer and Reference Manual”, Addison-Wesley, 2003.
[3]. Meihua xiao,jinyun xue, “Based on SPIN / Promela with the verification system”，Computer Science 8.201-204,2004
[4]. Huanming xhang，”Internet firewall security technology research and achieve” [J]，Micro-computer information，8-3 67-69,2006
[5]. D. Dolev and A. C. Yao. “On the security of public key protocols”. IEEE Transactions on www.51lunwen.org/computer/ information Theory, 29(2):198–208, 1983.
[6]. A. Josan本论文由英语论文网提供整理，提供论文代写，英语论文代写，代写论文，代写英语论文，代写留学生论文，代写英文论文，留学生论文代写相关核心关键词搜索。