Deciding Hedged Bisimilarity
Alessio Mansutti, Marino Miculan
TL;DR
This paper presents an algorithm to decide hedged bisimilarity in the spi-calculus, aiding the verification of cryptographic protocols by analyzing behavioral equivalences.
Contribution
It introduces a general algorithm for deciding hedged bisimilarity applicable to various encryption schemes in finite processes.
Findings
Algorithm successfully decides hedged bisimilarity.
Applicable to multiple encryption schemata.
Encompasses a broad class of behavioral equivalences.
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsAdvanced Authentication Protocols Security · Cryptographic Implementations and Security · Formal Methods in Verification