A Bisimulation Method for Automatic Confirmation of Network Security Cryptographic Protocols
Meng Hai · Journal of Neijiang Normal University · 2008
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 restriction,which arises from the process's receipt of infinite input,to finite migration,it helps secure the realization of the automatic security protocol confirmation that is based on such a relation.