Research On Formal Security Protocol Analysis Technology

Grid is an integrated computing resource infrastructure'that implements distributed resource coordination operations and guarantees a certain level of QoS to users based on standardized, open and common protocols and interfaces. Multi-user coordination computing in grid environment is an important research field. With the development of grid applications, higher system reliability is required. Security protocol is an important method for maintenance of system security. With the emergence of virtual organization (VO), the communication channel between users who handle the protocol is strongly related to VO, which means users realize the communication between each other by being authorized to join VO. Due to the hierarchy structure of VO management domain, protocol specified by VO may have process of parallel run in higher level VO context and there may exists parallel attack from dishonest entity. In this thesis, security requirments specification, formal analysis, counterexample constructing and attack eliminating for security protocol is studied based on gird VO.In this thesis, we propose a new efficient extension to the strand spaces model, by which shared state across the strands corresponding to the same agent is defined. Based on that, one method is given to separate protocol to atomic protocols in grid VO formally. Therefore, parallel attack can be eliminated through specifying and deploying dynamic authority policy to constrain the information pool action of dishonest entity in grid VO.This thesis presents the logic which is based on multi-agent system to specify various security properties. Moreover, this thesis extends the automatic proof search procedure in automated protocol verifier Athena for checking the validity of the well-formed formulas in the new logic. Due to the new constraint for restricting the communication of agents, the state space for our proof search procedure is reduced. Based on that, one method is provided to construct counterexample for protocol in VO automatically.One of the central challenges in the analysis of complex and industrial-size protocols is the expressiveness of the formalism used in the formal analysis and its capability to model complex cryptographic operations. While such protocols traditionally relied only on the basic cryptographic operations such as encryption and digital signatures, modern cryptography has invented more sophisticated primitives with unique security features that go far beyond the traditional understanding of cryptography to solely offer secrecy and authenticity of a communication. Secret share constitute such a prominent primitive. This thesis gives an abstraction of verifiable multi-secret sharing protocols that is accessible to a fully mechanized analysis. This abstraction is formalized within the applied pi-calculus by using an equational theory which characterizes the cryptographic semantics of secret share. An encoding from the equational theory into a convergent rewriting system in also presented, which is suitable for the automated protocol verifier ProVerif. Based on that, the threshold certificates protocol is analyzed。...