Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Probabilistic Bisimulation for Parameterized Anonymity and Uniformity Verification

Chih-Duo Hong, Anthony W. Lin, Philipp Rümmer, Rupak Majumdar

TL;DR

This work introduces a first-order framework based on the theory of regular structures to decide probabilistic bisimulation for parameterized infinite-state systems. By encoding systems, properties, and proofs in a decidable logic ($FO_\mathsf{reg}$) and adopting the minimal deviation assumption, the authors present decision procedures for anonymity and uniformity via regular bisimulations. A learning component with active automata learning automates the synthesis of candidate bisimulations, and padding/padding-related techniques enable handling of non-length-preserving behaviors. Case studies across cryptographic protocols and randomized algorithms demonstrate fully automated verification, illustrating the practical impact on verifying privacy and distributional properties in complex, infinite families of systems.

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.

Probabilistic Bisimulation for Parameterized Anonymity and Uniformity Verification

TL;DR

This work introduces a first-order framework based on the theory of regular structures to decide probabilistic bisimulation for parameterized infinite-state systems. By encoding systems, properties, and proofs in a decidable logic () and adopting the minimal deviation assumption, the authors present decision procedures for anonymity and uniformity via regular bisimulations. A learning component with active automata learning automates the synthesis of candidate bisimulations, and padding/padding-related techniques enable handling of non-length-preserving behaviors. Case studies across cryptographic protocols and randomized algorithms demonstrate fully automated verification, illustrating the practical impact on verifying privacy and distributional properties in complex, infinite families of systems.

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.
Paper Structure (38 sections, 11 theorems, 29 equations, 4 figures, 1 table, 2 algorithms)

This paper contains 38 sections, 11 theorems, 29 equations, 4 figures, 1 table, 2 algorithms.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Weighted transition system
  4. Bisimulation equivalence
  5. A first-order framework for regular relations
  6. Bisimulation in regular relations
  7. The non-weighted case
  8. Specifying and validating weighted systems
  9. Proof rules for bisimulation over weighted systems
  10. Learning-based bisimulation synthesis
  11. Active automata learning
  12. Learning regular bisimulations
  13. Membership queries $Mem(w)$
  14. Equivalence queries $Equ(\mathcal{A})$
  15. Padding WTS for bisimulation learning
  16. ...and 23 more sections

Key Result

Proposition 1

Two configurations of a WTS are bisimilar if and only if they satisfy the same PML formulas. Furthermore, it is decidable to check whether a configuration satisfies a PML formula in a finite WTS.

Figures (4)

  • Figure 1: Part of the configuration graph in Example \ref{['ex:pPDA']}, adapted from forejt2018game.
  • Figure 2: An overview of using automata learning to synthesize a bisimulation relation $R \supseteq E$. Here, $\ominus$ denotes symmetric set difference, $\tilde{R}$ is the greatest bisimulation relation, $\tilde{R}_n$ is $\tilde{R}$ restricted to configurations of size $n$, and $R$ denotes the relation represented by automata $\mathcal{A}$.
  • Figure 3: Example probabilistic programs for verifying probability uniformity and equivalence. We use $\oplus$ to denote the XOR Boolean operator, and use N to represent an unbounded natural number parameter. The function coin() returns 0 or 1 uniformly at random.
  • Figure 4: A Markov chain with uniform output distribution over $F_s = \{q_1, q_2\}$

Theorems & Definitions (23)

  • Proposition 1: bianco1995modelclerc2019expressiveness
  • Proposition 2: blumensath2004finitecolcombet2007transforming
  • Example 3
  • Theorem 4
  • proof
  • Example 5
  • Theorem 6
  • proof
  • Proposition 7: nerode1958linear
  • Proposition 8: rivest:inference1993
  • ...and 13 more