- 期刊
Extension of PCL Theory and Its Application in Improved CCITT X.509 Analysis
摘要
In the original PCL theory, due to the lack of a strict definition and inference rules of the relations among message subterms, the protocol analysis process was described as having neither rigor nor formalization, which seriously affected the accuracy of the analysis results. Secondly, The temporal ordering between the actions of the principals is the key basis for judging whether the principals correctly perform the roles of the protocol or not. The analysis on it based on timestamp mechanism which can directly reflect the temporal ordering of the actions of the principals, will greatly reduce the complexity of protocol analysis. However, there are no verification or inference rules based on the timestamp mechanism for the temporal relationship between the acts of protocol principals in the existing PCL theory. Accordingly, this paper is aimed to extend the PCL theory from two aspects: Message subterms relationship and timestamp mechanism. First, the inference rules of message subterms are given on the basis of a strict definition of the relations between message subterms. Secondly, based on the defined timestamp relations and the original PCL inference system, the rules for judging the temporal ordering of the receiving and sending behavior of protocol principals are given. To verify the validity of PCL extension theory, the conciseness of PCL in protocol security analysis and the correctness of improved CCITT X.509 protocol, a formal description of the improved CCITT X.509 protocol is given by using cue calculus language, and a formal description of the security properties of the protocol is given by using PCL logic. And then, the security analysis of the protocol is given by using the extended PCL theory in three areas: Authentication, confidentiality and data integrity. The process and results of protocol analysis show that the extended PCL theory can effectively reduce the complexity of protocol analysis, and the improved CCITT X.509 protocol can meet the goal of protocol security attribute design.