Seal演算的等式特性

为完善Seal演算的自身性质及形式化证明移动代码的安全性,从上下文等价性角度研究了Seal演算的等式特性及其应用。首先定义了Seal演算的可观察性和上下文等价性,然后通过两个判断上下文等价性的定理给出了Seal演算上下文等价性的判定方法,最后依据上下文等价性证明了Seal演算的防火墙等式。结果表明,Seal演算上下文等价性可以正确地描述Seal演算的等式特性,并可判定Seal演算的安全特性。