带否定的入侵者可推导性约束：可判定性及其在安全服务组合中的应用
密码学与安全
2012-07-23 v1
摘要
在我们先前的工作中，寻找用于组合安全服务的中介者问题已被归约为求解可推导性约束的问题，此类约束类似于密码协议分析中所采用的约束。本文通过一种构造扩展了中介者合成过程，用以表达某些数据对中介者不可访问。随后，我们给出了一种判定过程，用于验证满足此非披露策略的中介者是否可以被有效合成。该过程已在我们开发的协议分析工具 CL-AtSe 中实现。该过程显著扩展了用于密码协议分析的约束求解能力，因为它能够无限制地处理负向可推导性约束。特别是，它适用于所有子项收敛理论（subterm convergent theories），因此涵盖了形式化安全分析中的几种重要理论，包括加密、哈希、签名和配对。
引用
@article{arxiv.1207.4871,
title = {Intruder deducibility constraints with negation. Decidability and application to secured service compositions},
author = {Tigran Avanesov and Yannick Chevalier and Michaël Rusinowitch and Mathieu Turuani},
journal= {arXiv preprint arXiv:1207.4871},
year = {2012}
}
备注
(2012)