Abstract: As a method of security protocols formal modeling, MultiSet Rewriting(MSR) model offers an academic scheme, but is not perfect. Aiming at the lack of checking in type flaw, this paper improves the MSR model, expands the content of type, enriches the deduction rule, so that it can detect a certain type of attackand. It describes the security attributes, and the examples verify the non-repudiation and fairness of the exchange protocols based on MSR model.

Key words: MultiSet Rewriting(MSR) model, security protocol, non-repudiation, fairness

摘要： 作为安全协议形式化建模方法之一的多集重写(MSR)模型虽然提供了基本的理论框架，但并不完善。针对其在类型攻击检测方面的不足，对原模型进行改进，扩展类型内容，丰富推演规则，使其能检测特定类型的攻击。给出安全属性的描述，并用实例验证扩展后的MSR模型中交换协议的非否认性和公平性。

关键词: 多集重写模型, 安全协议, 非否认性, 公平性

CLC Number: 

• TP309