



























Given a probabilistic transition system (PTS) $\cal A$ partially observed by an attacker, and an $ω$-regular predicate $\varphi$over the traces of $\cal A$, measuring the disclosure of the secret $\varphi$ in $\cal A$ means computing the probability that an attacker who observes a run of $\cal A$ can ascertain that its trace belongs to $\varphi$. In the context of refinement, we consider specifications given as Interval-valued Discrete Time Markov Chains (IDTMCs), which are underspecified Markov chains where probabilities on edges are only required to belong to intervals. Scheduling an IDTMC $\cal S$ produces a concrete implementation as a PTS and we define the worst case disclosure of secret $\varphi$ in ${\cal S}$ as the maximal disclosure of $\varphi$ over all PTSs thus produced. We compute this value for a subclass of IDTMCs and we prove that refinement can only improve the opacity of implementations.
此内容由惯性聚合(RSS阅读器)自动聚合整理,仅供阅读参考。 原文来自 — 版权归原作者所有。