Definition. Observational equivalence for a declared protocol [ftip-007R]
Definition. Observational equivalence for a declared protocol [ftip-007R]
Let \(\mathcal T_{\mathsf P}\) be the finite set of possible transcripts for a declared protocol \(\mathsf P\). Two feedback worlds \(w_0,w_1\) are observationally equivalent for \(\mathsf P\), written \(w_0\equiv _{\mathsf P}w_1\), when
\[ \Pr (T_{w_0}^{\mathsf P}=t)=\Pr (T_{w_1}^{\mathsf P}=t) \qquad \text {for every }t\in \mathcal T_{\mathsf P}. \]The relation is protocol-relative. Another protocol may issue a different feedback request and thereby separate the same worlds. Equality only on the realized transcript is weaker than this definition, which compares the whole finite transcript law.