We demonstrate the flaws of Mao's method, which is an augmentation ofprotocol idealization in BAN-like logics, and then offer some new idealization rules based on Mao'smethod. Furthermore, we give some theoret...We demonstrate the flaws of Mao's method, which is an augmentation ofprotocol idealization in BAN-like logics, and then offer some new idealization rules based on Mao'smethod. Furthermore, we give some theoretical analysis of our rules using the strand spaceformalism, and show the soundness of our idealization rules under strand spaces Some examples onusing the new rules to analyze security protocols are also concerned. Our idealization method ismore effective than Mao's method towards many protocol instances, and is supported by a formalmodel.展开更多
The modified version of Yahalom protocol improved by Burrows, Abradi, and Needham （BAN） still has security drawbacks. This study analyzed such flaws in a detailed way from the point of strand spaces, which is a nove...The modified version of Yahalom protocol improved by Burrows, Abradi, and Needham （BAN） still has security drawbacks. This study analyzed such flaws in a detailed way from the point of strand spaces, which is a novel method of analyzing protoeol＇s security. First, a mathematical model of BAN-Yahalom protocol is constructed. Second, penetrators＇ abilities are restricted with a rigorous and formalized definition. Moreover, to increase the security of this protocol against potential attackers in practice, a further improvement is made to the protocol. Future application of this re-improved protocol is also discussed.展开更多
Security protocol is specified as the procedure of challenge-response, which uses applied cryptography to confirm the existence of other principals and fulfill some data negotiation such as session keys. Most of the e...Security protocol is specified as the procedure of challenge-response, which uses applied cryptography to confirm the existence of other principals and fulfill some data negotiation such as session keys. Most of the existing analysis methods, which either adopt theorem proving techniques such as state exploration or logic reasoning techniques such as authentication logic, face the conflicts between analysis power and operability. To solve the problem, a new efficient method is proposed that provides SSM semantics-based definition of secrecy and authentication goals and applies authentication logic as fundamental analysis techniques, in which secrecy analysis is split into two parts： Explicit-lnformaUon-Leakage and Implicit-Information-Leakage, and correspondence analysis is concluded as the analysis of the existence relationship of Strands and the agreement of Strand pa- rameters. This new method owns both the power of the Strand Space Model and concision of authentication logic.展开更多
文摘We demonstrate the flaws of Mao's method, which is an augmentation ofprotocol idealization in BAN-like logics, and then offer some new idealization rules based on Mao'smethod. Furthermore, we give some theoretical analysis of our rules using the strand spaceformalism, and show the soundness of our idealization rules under strand spaces Some examples onusing the new rules to analyze security protocols are also concerned. Our idealization method ismore effective than Mao's method towards many protocol instances, and is supported by a formalmodel.
基金supported by the National Natural Science Foundation of China(6057314,60773041)
文摘The modified version of Yahalom protocol improved by Burrows, Abradi, and Needham （BAN） still has security drawbacks. This study analyzed such flaws in a detailed way from the point of strand spaces, which is a novel method of analyzing protoeol＇s security. First, a mathematical model of BAN-Yahalom protocol is constructed. Second, penetrators＇ abilities are restricted with a rigorous and formalized definition. Moreover, to increase the security of this protocol against potential attackers in practice, a further improvement is made to the protocol. Future application of this re-improved protocol is also discussed.
基金National Natural Science Foundation of China (Grant Nos. 90412014 and 90604004)Jiangsu Provincial Key Laboratory of Network and Information Security (Grant No. BM2003201)Jiangsu Provincial High-Tech Research Program (Grant No. BG2004036)
文摘Security protocol is specified as the procedure of challenge-response, which uses applied cryptography to confirm the existence of other principals and fulfill some data negotiation such as session keys. Most of the existing analysis methods, which either adopt theorem proving techniques such as state exploration or logic reasoning techniques such as authentication logic, face the conflicts between analysis power and operability. To solve the problem, a new efficient method is proposed that provides SSM semantics-based definition of secrecy and authentication goals and applies authentication logic as fundamental analysis techniques, in which secrecy analysis is split into two parts： Explicit-lnformaUon-Leakage and Implicit-Information-Leakage, and correspondence analysis is concluded as the analysis of the existence relationship of Strands and the agreement of Strand pa- rameters. This new method owns both the power of the Strand Space Model and concision of authentication logic.
