Security Analysis Of Cryptographic Protocols Based On Fine-Grained Freshness

With the rapid development of the internet, the security protocol, which is based on internet, is becoming more and more important. This article is to improve and extend the method of Belief Multiset Formalism for Cryptographic Protocol Analysis, which is based on freshness, so we propose the improved method - Security Analysis of Cryptographic Protocols Based on Fine-Grained Freshness.In this method, we put forward the fine-grained definitions of both freshness and secrecy. Many concepts have been defined clearly here, such as freshness, trusted freshness, verifiable freshness, private secret, trusted private secret, verifiable private secret, onymous message and implicit share secret, and so on. With these concepts, the assumption and the security target can be defined finely and clearly in protocol's analysis. Based on these concepts, we construct some rules to analyze two-party key-establishment protocol, and every rule has the semantic explanation, which makes the rule more explicit and understandable.Besides, we also provide a clear assumption on the third trusted party S, whose assumption is much clearer and more reasonable than before, and then we use this extended method to analyze key-establishment protocols with trusted party S.At last, we use this improved method (Security Analysis of Cryptographic Protocols Based on Fine-Grained Freshness) to analyze both Helsinki protocol and Yahalom Protocol respectively. When analyzing Helsinki protocol, we find a serious weakness and we also give an explanation on this weakness. However, what we have explained is different from what Mitchell has explained in his article. By comparing with each other, we find the Mitchell's explanation is not correct. We correct his explanation and give a reasonable explanation. In the analysis of Yahalom protocol, we also find a subtle weakness in the protocol. However, due to the lack of fine-grained definitions on freshness, the method of"Belief Multiset Formalism for Cryptographic Protocol Analysis"can not find out this subtle weakness.