Towards the Idealization Procedure of BAN-Like Logics

摘要

We demonstrate the flaws of Mao's method, which is an augmentation of protocol idealization in BAN-like logics, and then offer some new idealization rules based on Mao's method. Furthermore, we give some theoretical analysis of our rules using the strand space formalism, and show the soundness of our idealization rules under strand spaces Some examples on using the new rules to analyze security protocols are also concerned. Our idealization method is more effective than Mao's method towards many protocol instances, and is supported by a formal model.