Dissertation > Excellent graduate degree dissertation topics show

Research on Formal Security Protocol Analysis Technology

Author: ZhaoHui
Tutor: LiMingChu
School: Dalian University of Technology
Course: Applied Computer Technology
Keywords: Grid Collaborative Computing Security model Security protocol Formal Analysis
CLC: TP393.08
Type: PhD thesis
Year: 2010
Downloads: 225
Quote: 0
Read: Download Dissertation

Abstract

Grid computing resources is an integrated environment, through a standard, open, general-purpose protocols and interfaces to achieve the collaborative use of distributed resources, and its ability to provide users with a non-trivial quality of service. Collaborative computing in which the participation of multi-user grid environment is an important application of the grid. At the same time, the development of the grid for the reliability of operation put forward higher requirements, the security agreement is an important means to guarantee security. Grid environment, the security protocol running in the communication between the entities primarily through virtual organizations to achieve certification and authorization, that user must join virtual organizations to achieve with other members of the virtual organization to communicate between. Grid virtual organization security protocols may exist with other security agreement between the grid virtual organization has a hierarchical management structure, to run in parallel. Although the majority of security protocols to meet the security objectives, non-honest entities might be interested in the security protocol implementation of parallel attack. Formal analysis and verification of security protocols based on grid virtual organization of in-depth research, the main contents include: security needs formal description, analysis and verification of security protocols, attacks automation structure, and attacks to eliminate counter-examples. Completed work: through this article introduced the concept of grid computing agents in the the traditional strand space model based on the security protocol participants and virtual organization in grid computing agent linked to a new grid virtual organizational environment, formal analysis and verification of security protocols, as well as a grid virtual organization-based security protocols formalized split. And on this basis put forward a grid virtual organization environment, development and deployment of two dynamic authorization policy by limiting the protocol participants concerted practices that may exist between the split sub-protocol ultimately achieve the elimination of non-honest participants grid virtual organization environment security protocol parallel attack. The paper also proposed security protocol split method successfully eliminates grid virtual organization environment under a parallel attack mutual authentication protocol for Diffie-Hellman. Athena Security Agreement automatic verification tools based on the traditional strand space model automated verification of security protocols. And the traditional strand space model can not be defined subordinate to the sharing of information between the different strings of the same agent, Athena security protocols automated verification tool can not complete structure grid virtual parallel attacks counter-example of the security agreement non-honest participants in the organizational environment. In this paper, in the traditional strand space model based on the introduction of the concept of grid computing, agent, extended security attributes defined in the Athena security protocols automated validation tools and safety evidence derivation, making new logical system capable of supporting a multi-agent system, This largely reduces the state explosion phenomenon exists in the original system. On this basis, this paper proposes a new grid virtual organization environment under the security agreement to attack the counter-example of automated construction method. At the same time using the proposed automated method to construct a counter-example of bi-directional authentication protocol for Diffie-Hellman attack grid virtual organization environment. The current security protocol analysis of one of the major challenges faced by the technology in the form of how the formal definition of complex cryptographic operations. Traditional security protocol analysis technology is only a formal definition of basic cryptographic operations, including encryption and digital signatures, including such basic cryptographic operations only possess certification with secret security attributes. Modern security protocols, many new cryptographic operations, such cryptographic operations with a more complex operation than the basic password security attributes. Secret Sharing belongs to a class of cryptographic operations. Based equivalents theoretical cryptography verifiable multi-secret sharing scheme in the application of Pi calculus semantics formal definition. On this basis, the paper further proposed a method for the proposed limited equivalents theory into security protocol automation the validator Proverif in, rewrite mechanism coding method, and, eventually realized in the Proverif verifiable multi-secret Formal verification sharing scheme. Using the proposed finite equivalent theory on thresholds in the Proverif certificate protocol was validated.

Related Dissertations

CLC: > Industrial Technology > Automation technology,computer technology > Computing technology,computer technology > Computer applications > Computer network > General issues > Computer Network Security
© 2012 www.DissertationTopic.Net Mobile