arXiv · 1611.03424
Deciding Hedged Bisimilarity
Abstract
The spi-calculus is a formal model for the design and analysis of cryptographic protocols: many security properties, such as authentication and strong confidentiality, can be reduced to the verification of behavioural equivalences between spi processes. In this paper we provide an algorithm for deciding hedged bisimilarity on finite processes, which is equivalent to barbed equivalence (and coarser than framed bisimilarity). This algorithm works with any term equivalence satisfying a simple set of conditions, thus encompassing many different encryption schemata.
Explore related subjects
Keep this discovery
Alessio Mansutti, Marino Miculan. 2016-11-10. Deciding Hedged Bisimilarity. https://arxiv.org/abs/1611.03424
Cite the original work for its findings. Save a collection to share your selection of sources.