Advertisement
Published in:
2005 | OriginalPaper | Chapter
Towards a Symbolic Bisimulation for the Spi Calculus
Authors : Yinhua Lü, Xiaorong Chen, Luming Fang, Hangjun Wang
Published in: Mobile Ad-hoc and Sensor Networks
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
Observational equivalence is a powerful means for formulating the security properties of cryptographic protocols. However suffering from the infinite quantifications over contexts, its proof becomes notoriously troublesome. This paper addresses the problem with a symbolic technique. We propose a symbolic bisimulation for spi calculus based on an environmental sensitive label transition system semantics, which restrict the infinite inputs of a process to only finite transitions. We also prove that the symbolic bisimulation is sound to the traditional concrete bisimulation, and furthermore is a promising means to automatically verifying the security protocols.