一种基于串空间的不变集生成算法

A new algorithm for constructing invariant-sets based on strand spaces

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

The ideal is defined as an algebraic structure of invariant-sets in a strand space model, where thekey procedure of a formal analysis of security protocols can be regarded as constructing some invariant-sets, i. e. algebras. The bounds on the abilities of the penetrator are described using the properties of ideals. In this paper, we define the mapping hash：K×B^n-1→B and extend the sub-term relations in the original model. We also obtain that the decidable theorem for honesty of ideals still holds as it is described under the extended subterm relations. Finally, the theorem for the satisfiability of decidable conditions of honest ideals and a new al- gorithm for constructing invariant-sets are proposed.