基于PI演算的反XML重写攻击安全模型验证

Verifying the Counter XML Rewriting Attacks Model Based on PI-Calculus

设计出一个安全模型后,要严格验证其是否满足安全需求是非常重要和必要的。利用形式化方法来检验模型是否满足了安全协议是一种有效的手段。本文针对XML重写攻击,设计出了一个反XML重写攻击的安全模型,然后运用Pi演算形式化方法验证了其有效性、真实性和安全性。

It is very important and necessary to check the security of a model. And it is effective to use formal methods to verify the model. In this paper, we use pi - calculus to verify availability, authenticity and security properties of Counter XML Rewriting Attack Model.