Research On Formal Methods And Their Applications For Security Protocols

Networks can make people access shared network resources by any ways and at any place and any time, meanwhile through networks being rapidly developed and its application being gradually extended, there exist more and more security threats in networks,in order to guarantee that networks are running securely, and resources can be securely utilized, security protocols, as the basis of security services in networks, are paid more attention, but because security protocols are very complex, its theory and engineering technology are not perfect, together with scientists and engineers have limited ability to perceive, so there exist security vulnerabilities in present security protocols. In order to design more valid security protocols, the formal method become the valid tool to describe, design and analyze security protocols, in which the logic method has been researched quite deeply, and has been applied widely and successfully. There exist security vulnerabilities at different extents in various security protocols of present wireless local networks; especially there exist fatal security holes in the security mechanisms of 802.11. Recently in order to create the future computer system in which the high security is based on characteristics of trusted platforms, the trusted computing group has put forward the secure architecture which is based on secure chip on hardware platforms of computers and can increase security guarantees of computer systems through the security of hardware. In the dissertation, I deeply research agent oriented formal description, design and analysis for security protocols, and research the authentication and key agreement protocol of wireless authentication and privacy infrastructure and the object independent authorization protocol of trusted computing utilizing the agent oriented methods for formally describing, designing and analyzing security protocols which is put forward in the dissertation. The main contributions of the dissertation include,(1) In the research of the agent oriented logical language to describe security protocols,I regard the process of agents by exchanging messages following the security protocols as the process of exchanging their possession, knowledge and belief and as the process of monotonously increasing their possession, knowledge and belief following time; I make the formal language for specification of security protocols based on possession, knowledge, belief, sending, receiving and time, and make its Kripke semantic model and interpretation of true value; describe agents'characteristics and roles with agent oriented formal method, quite clearly, wholly and exactly specify the recognizability and freshness of messages, the attributes...