基于细化建模的概率不透明性
密码学与安全
2015-10-16 v1
摘要
给定一个被攻击者部分观察的概率转移系统（PTS），以及关于轨迹的-正则谓词，测量中秘密的披露意味着计算观察到一次运行的攻击者能够确定其轨迹属于的概率。在细化背景下，我们考虑以区间值离散时间马尔可夫链（IDTMC）形式给出的规范，它们是欠指定的马尔可夫链，其中边上的概率仅被要求属于区间。调度IDTMC 产生一个具体实现作为PTS，我们将中秘密的最坏情况披露定义为在所有由此产生的PTS上披露的最大值。我们计算了IDTMC子类上的该值，并证明细化只能改善实现的不透明性。
引用
@article{arxiv.1510.04316,
title = {Probabilistic Opacity in Refinement-Based Modeling},
author = {Béatrice Bérard and Olga Kouchnarenko and John Mullins and Mathieu Sassolas},
journal= {arXiv preprint arXiv:1510.04316},
year = {2015}
}