Dynamic Logic Method Based on Message Unique Origin
Zhou Ming-tian · Dianzi xuebao · 2007
A new logic method for analyzing security protocols was presented in this paper.A dynamic model was presented,which overcame the flaw of the BAN-like logic in its protocol idealization step.The basic concept of Message Unique Origin(MUO) and its determinant rules ware presented,which could be used to distinguish between sound trust and unsound trust.The difference between believe the occurrence of the event and believe the truth of the event was resolved.Based on the concept of MUO,a new dynamic logic is build up,whose validity is proved by an example protocol which is soundness in the BAN-like logic but is found to have some flaws by this dynamic logic.