一种自动验证网络安全协议的互模拟方法  

A Bisimulation Method for Automatic Confirmation of Network Security Cryptographic Protocols

作　　者：杨军[1] 孟海涛[1] 

机构地区：[1]盐城工学院,江苏盐城224051

出　　处：《内江师范学院学报》2008年第12期56-58,共3页Journal of Neijiang Normal University

摘　　要：为了解决进程接收具体信息的输入所带来的无穷种迁移问题,采用一种称为"符号化"的方法,提出了进程符号环境和符号化和格局标号迁移语义,为Spi演算设计了符号互模拟关系—符号Reded互模拟.结果表明:该符号互模拟关系对传统的互模拟关系是可靠的,符号化的标号转移语义将进程无穷输入导致的迁移限期为有穷种迁移.因此使得基于该关系的安全协议自动验证算法得以实现.In order to find a solution to the infinite migration problem caused by a process s receipt of concrete information input,by use of a symbolic method,the idea of process symbolic environment and symbolic migration semantics are put forth.The relation of symbolic bisimulation(symbolic Reefed bisimulation) is designed for Spi calculus.The result shows: the symbolic bisimulation is reliable to the traditional concrete bisimulation.Since the symbolic migration semantics is able to confine the migration restrict...

关 键 词：密文通信协议 进程演算 符号互模拟 

分 类 号：TP393.08[自动化与计算机技术—计算机应用技术]