论文部分内容阅读
针对安全协议安全属性是否满足，缺乏有效性能评价方法的现状，大都使用SPI演算或相近的进程代数方法进行建模。利用这种方法不仅能够有效地形式化描述安全协议，并且能够对安全协议进行多方面的系统评价，但基本上没有说明怎么样寻找设计合适的验证工具，验证其安全属性实现的正确性。本文引入基于SPI演算的验证工具SPRITE来保证建模过程正确性，并设计给出实现映射的具体方法。本方法通过对典型的WOO-LAM单向认证协议予以说明，最后SPRITE产生的具体JAVA代码，给出了安全协议的安全属性，使形式化描述的协议的安全属性