论文部分内容阅读
在串空间模型中将理想定义为其不变集的代数结构，并利用它的性质描述攻击者攻击行为的能力界限。将安全协议的形式化分析规约为代数系统的不变集生成,引入hash：K×B^n-1→B，扩充了原模型中的子句关系，并给出理想诚实性判定定理在扩充子句关系下仍成立的结论．在此基础之上，提出诚实性判定条件的可满足性定理和一种新的不变集生成算法．