Probabilistic Bisimulation for Parameterized Anonymity and Uniformity Verification

TL;DR

This paper introduces a logical framework based on the first-order theory of regular structures for verifying probabilistic bisimulation, anonymity, and uniformity in parameterized systems, enabling fully automated proofs for complex probabilistic models.

Contribution

It presents a novel decidable logic framework for analyzing bisimulation in infinite families of probabilistic systems, integrating language inference for automation.

Findings

Successfully verified cryptographic protocols and randomized algorithms

Achieved full automation in synthesizing bisimulation proofs

Demonstrated effectiveness on complex probabilistic models

Abstract

Bisimulation is crucial for verifying process equivalence in probabilistic systems. This paper presents a novel logical framework for analyzing bisimulation in probabilistic parameterized systems, namely, infinite families of finite-state probabilistic systems. Our framework is built upon the first-order theory of regular structures, which provides a decidable logic for reasoning about these systems. We show that essential properties like anonymity and uniformity can be encoded and verified within this framework in a manner aligning with the principles of deductive software verification, where systems, properties, and proofs are expressed in a unified decidable logic. By integrating language inference techniques, we achieve full automation in synthesizing candidate bisimulation proofs for anonymity and uniformity. We demonstrate the efficacy of our approach by addressing several challenging examples, including cryptographic protocols and randomized algorithms that were previously beyond the reach of fully automated methods.