Stateful applied pi calculus: Observational equivalence and labelled bisimilarity
Stateful applied pi calculus: Observational equivalence and labelled bisimilarity
复制标题
有状态应用 pi 演算：观察等价性和标记的双相似性
DOI：
10.1016/j.jlamp.2017.03.001
复制
发表时间：
2017
影响因子：
0.9
通讯作者：
Arapinis M
中科院分区：
文献类型：
--
作者：
Arapinis M
我们扩展了Abadi-Fournet的应用π演算与状态细胞，这是用来存储持久性信息的协议的原因。例如涉及数据库或具有内部状态的硬件模块的协议。我们区分私人状态细胞，这是不可用的攻击者，和公共状态细胞，当一个私人状态细胞被攻击者妥协时出现。对于只涉及私人状态细胞的过程，我们定义观测等价性和标记的双相似性，以相同的方式在原来的应用π演算，并表明它们是一致的。我们的结果意味着阿巴迪-富内定理-观测等价性和标记的双相似性的巧合-在一个修订版的应用π演算。对于涉及公共状态单元的过程，我们基本上可以保留观测等价的定义，但需要加强标记互模拟的定义，以表明在这种情况下观测等价和标记互相似也是一致的。
We extend Abadi–Fournet's applied pi calculus with state cells, which are used to reason about protocols that store persistent information. Examples are protocols involving databases or hardware modules with internal state. We distinguish between private state cells, which are not available to the attacker, and public state cells, which arise when a private state cell is compromised by the attacker. For processes involving only private state cells we define observational equivalence and labelled bisimilarity in the same way as in the original applied pi calculus, and show that they coincide. Our result implies Abadi–Fournet's theorem – the coincidence of observational equivalence and labelled bisimilarity – in a revised version of the applied pi calculus. For processes involving public state cells, we can essentially keep the definition of observational equivalence, but need to strengthen the definition of labelled bisimulation in order to show that observational equivalence and labelled bisimilarity coincide in this case as well.
登录
查看更多内容
DOI：
--
发表时间：
2002
期刊：
International Symposium on Privacy Enhancing Technologies
影响因子：
--
作者：
M. Abadi
通讯作者：
M. Abadi
DOI：
10.1109/sp.2008.23
发表时间：
2008-05
期刊：
2008 IEEE Symposium on Security and Privacy (sp 2008)
影响因子：
--
作者：
M. Backes;Matteo Maffei;Dominique Unruh
通讯作者：
M. Backes;Matteo Maffei;Dominique Unruh
YAPA：计算入侵者知识的通用工具
DOI：
--
发表时间：
2009
期刊：
TOCL
影响因子：
--
作者：
M. Baudet;V. Cortier;S. Delaune
通讯作者：
S. Delaune
DOI：
10.1016/j.tcs.2012.07.034
发表时间：
2009-12
期刊：
Theor. Comput. Sci.
影响因子：
--
作者：
Jia Liu;Huimin Lin
通讯作者：
Jia Liu;Huimin Lin
应用Pi演算中标记双相似性与观察等价性的一致证明
DOI：
--
发表时间：
2011
期刊：
影响因子：
--
作者：
Jia Liu
通讯作者：
Jia Liu