关键词: 安全协议, 协议目标, 协议度量, 协议冗余, 模态逻辑

Abstract: In order to introduce the quantitatively analytical method into security protocol analysis‚a protocol measurement method based on modal logic was defined．This method formally specifies the parameters and approaches to measure the satisfaction of security goals of the protocol contents．On this basis‚approaches of mea-suring protocol redundancy and corresponding simplification were then put forward．The method was finally applied to analyze a sample protocol‚describe the contribution of each protocol content and present the inefficacy of redundancy factors to protocol targets‚thus achieving the safe simplification．The method is possessed of a main feature of applying quantitative analysis to the formal analysis of security protocol‚and of the advantages and limitations of modal logic methods.

Key words: security protocol, protocol goal, protocol measurement, protocol redundancy, modal logic