基于逻辑程序的安全协议验证

被引:6
作者
李梦君
李舟军
陈火旺
机构
[1] 国防科学技术大学计算机学院,国防科学技术大学计算机学院,国防科学技术大学计算机学院长沙,长沙,长沙
关键词
安全协议; 逻辑程序; 不动点; 验证策略;
D O I
暂无
中图分类号
TP393.08 [];
学科分类号
0839 ; 1402 ;
摘要
安全协议本质上是分布式并发程序 ,可以自然地描述为多个子进程的并发合成系统 .将安全协议对应的并发合成系统抽象为逻辑程序进行消解 ,能够对安全协议无穷多个会话的交叠运行进行验证 .该文提出了安全协议逻辑程序中逻辑规则的一个分类方法 ,基于该分类方法提出了安全协议逻辑程序不动点的迭代计算方法 .逻辑规则的分类优化了安全协议逻辑程序不动点的迭代计算和安全性质验证过程中的计算 .由于安全协议逻辑程序不动点迭代计算过程不一定终止 ,文中提出了每进行k 1步安全协议逻辑程序不动点迭代计算验证一次安全性质的验证策略 .
引用
收藏
页码:1361 / 1368
页数:8
相关论文
共 7 条
[1]  
An efficient cryptographic protocol verifier based on logic programming. Blanchet B. In: Proceedings of the 14th Computer Security Foundation Workshop, Cape Breton, Nova Scotia, Canada . 2001
[2]  
On the security of public key protocols. Dolev D,Yao A. IEEE Transactions on Information Theory . 1983
[3]  
A hierarchy of authentication specifications. Lowe G. In: Proceedings of the 10th Computer Security Foundation Workshop,Massachusetts, USA . 1997
[4]  
Analyzingsecurityprotocolswithsecrecytypesandlogicprograms. AbadiM,BlanchetB. Proceedingsofthe29thACMSym posiumonPrinciplesofProgramingLanguages (POPL’’02) . 2002
[5]  
Acalculusforcryptographicprotocols:Thespicalculus. AbadiM,GordonA .D. InformationandComputatiuon . 1999
[6]  
Fastandpreciseregularapproxima tionsoflogicpograms. GallagherJ,deWaalD .A. Proceedingsofthe11thInternationalConferenceonLogicProgramming . 1994
[7]  
From secrecy to authenticity in security protocols. Blanchet B. In:Proceedings of the 9th International Static Analysis Symposium,Madrid . 2002