Bisimilarity in the Spi-Calculus
Authors
Frendrup, Ulrik ; Jensen, Jesper Nyholm
Term
4. term
Education
Publication year
2001
Abstract
Spi-calculus er en matematisk ramme til at beskrive og verificere sikkerhedsprotokoller—formelle modeller af, hvordan parter udveksler beskeder sikkert. Korrekthed udtrykkes ofte som adfærdsmæssig ækvivalens: to protokolbeskrivelser betragtes som ens, hvis ingen ekstern observatør kan skelne dem ved at interagere med dem. Et naturligt valg er test-ækvivalens, men det er svært at bevise i praksis. Derfor er der foreslået alternative ækvivalenser, som er lettere at arbejde med. Abadi og Gordon introducerede framed bisimilarity, og Boreale m.fl. introducerede environment sensitive bisimilarity. Begge er kendt som forsvarlige approksimationer af may-testing-ækvivalens. I denne afhandling viser vi, at framed bisimilarity og en strong late version af environment sensitive bisimilarity faktisk er den samme relation. Vi definerer også en early variant af framed bisimilarity, kaldet frameless framed bisimilarity, og viser, at den falder sammen med strong early environment sensitive bisimilarity. Endelig foreslår vi modallogikker for Spi-calculus og viser, at strong early og strong late environment sensitive bisimilarity kan karakteriseres af disse logikker.
The spi-calculus is a mathematical framework for describing and verifying security protocols—formal models of how parties exchange messages securely. In this setting, correctness is often expressed as behavioral equivalence: two protocol descriptions are the same if no external observer can tell them apart by interacting with them. A natural choice is testing equivalence, but it is hard to prove in practice. As a result, researchers have proposed alternative equivalences that are easier to work with. Abadi and Gordon introduced framed bisimilarity, and Boreale et al. introduced environment sensitive bisimilarity. Both are known to be sound approximations of may-testing equivalence. This thesis shows that framed bisimilarity and a strong late version of environment sensitive bisimilarity are actually the same relation. We also define an early variant of framed bisimilarity, called frameless framed bisimilarity, and prove that it coincides with strong early environment sensitive bisimilarity. Finally, we propose modal logics for the spi-calculus that characterize these relations, so that strong early and strong late environment sensitive bisimilarity can be captured by suitable logical formulas.
[This abstract was generated with the help of AI]
Documents