The Formal Analysis And Control To Security Protocol Of Telecommunication For Electric Power System

Power telecommunication is the important composing of power system, and the security command of the communication includes authentication, access control, firewall, and so on, which the realization depended on the security protocol. The security protocol is an alternating protocol that is based on the encryption, and it is the crucial guarantee of power communication system. Howerer, it is difficult to design a security that match the security object. Reviewing the development of security protocol, it is always designing a protocol firstly, and then modifying it if some weakness was discovered, some weaknesses were found ten years later when the protocol was designed. So, it needs some methods help to design a security protocol, and analyse the protocol. The analysise approaches were focused on in this thesis.The automation analysis is always the aim of researchers, and the formal analysis is the base of it. The automation analysis can be realized based on the formal analysis, through the formal description language. This thesis is the basic research of automation analysis for which the BAN (Burrows Abadi Needham Logic) logic and strand space were adopted. The protocols were abstracted in different mathematics format, and the security of the protocol was analysised based on these models. The main contribution of this work is as follows: The first is that the AODV protocol was abstracted through BAN logic, and the security was confirmed based on it. The second is that the Hesinki protocol was modeled through the strand space, and the attack manner and the min-idea were analysised to confirm the security of the protocol.