模型检验 1/36 高级软件工程第八讲模型检验主要考虑如何发现设计缺陷！1模型检验 2/36 高级软件工程一、例子二、模型检测概述三、模型检测算法概览四、模型检测工具内 容2模型检验 3/36 高级软件工程Needham-Schroeder 身份认证协议N, S1ZS1, S2NS2Z通信过程可能被窃听！加密可以防止窃听！如何约定加密数字？每人 有自己的标识：N每人 公布自己的公钥: 只有N 才能解开的消息： *N每个对话过程 用一对数字对内容加密: S1, S2每次对话前 需要首先建立这对数字该协议于1978年被提出并得到广泛应用NZ一、例子3模型检验 4/36 高级软件工程N, S1WS1, S2NS2WN, S1ZS1, S2NS2Z1996年，发现该协议存在设计缺陷：攻击者可以伪装一方的身份利用模型检测方法！被欺骗！不可信！开始伪装Z W N4模型检验 5/36 高级软件工程In 1992 Clarke and his students at CMU used SMV to verify the IEEE Future+ cache coherence protocol. Th
