随着计算机技术的发展,其安全问题也日益凸显,解决该类问题的一个有效方法是模型检测。模型检测常用LTL和CTL公式表示待验证的性质。LTL公式更易于表达,CTL公式则采用较高效的符号模型检测技术。由于LTL公式并不能直接使用符号模型检测技术,为了提高LTL公式模型检测的速度,扩大处理规模,本文研究将LTL转化为公平性约束条件下的CTL模型检测的方法。主要工作有如下几点:(1)给出了将LTL的公式检验转化为公平性约束条件下的CTL模型检测的算法:首先构造待验证性质和待验证系统的Kripke结构和,再将和作积得到新的Kripke结构,然后在0)上加上相关公平性约束之后,在上进行模型检测,使得对LTL的公式检验转化为CTL公式。最后给出了该方法的正确性证明。(2)为了验证上述方法,对Hash-lock协议进行模型检测。首先给出了一个针对Hash-lock协议的攻击者模型;然后分别使用LTL公式和转化之后CTL公式对该协议进行模型检测,验证了该种算法的有效性,对比实验结果显示转化后的CTL模型检测效率更高。(3)应用模型检测工具nuXmv对Hash-lock协议进行形式化建模与分析,验证Hash-lock协议的两个性质。通过对模型检测结果的分析,发现了该协议的一个漏洞。