发表机构
Georgia Institute of Technology; Vachani School of Advanced Computing, Ashoka University（佐治亚理工学院; 阿育王大学瓦查尼高等计算学院）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文针对协议验证中目标所需的最弱信任假设问题，提出通过停止最小攻击的最小方式集合来精确刻画，并利用伽罗瓦连接统一解释，给出计算算法及 NP 困难性，实验验证了方法的有效性。
AI 中文摘要
协议验证器在给定的信任假设下（例如密钥从未泄露、值是新鲜的或信道是真实的）检查协议是否达到安全目标。它们并不说明目标需要哪些假设。Rowe、Guttman 和 Liskov 提出了在哪些最弱假设下协议能达到目标的问题，并留下了开放问题。我们针对关于密钥、值和信道的假设回答了该问题。将违反目标的运行称为攻击，将能排除该攻击的假设称为其停止集。协议为达到目标所必须信任的最少内容，正是停止其所有最小攻击的最小方式集合。可能存在多个这样的集合。当允许或/或假设时，答案变得唯一，并且当每个最小攻击都被单个假设停止时，答案恰好是一个集合。假设与目标之间的伽罗瓦连接解释了原因：目标可能以“或”结尾，但其假设可能不会。相同的结构给出了目标合取所需的信任，以及组合协议无需额外信任的精确条件。为了计算答案，一个循环询问验证器候选假设是否足够，记录每个报告攻击的停止方式，并重新计算候选假设。判断最多 k 个假设的信任是否足够是 NP 困难的。使用我们自己的有界分析器和 CPSA，该循环为十个协议及其变体上的 18 个目标找到了最弱信任，并且在每个目标上，它与使用相同验证器评估所有信任的结果一致。答案包括一个假设，即我们采用的 Kerberos PKINIT 修复模型所陈述的，但客户端对服务器的认证并不需要该假设，以及在有界模型下 Needham-Schroeder 达到其目标的信道假设。
英文摘要
Protocol verifiers check whether a protocol meets a security goal under stated trust assumptions, such as that a key is never leaked, a value is fresh, or a channel is authentic. They do not say which of those assumptions the goal needs. Rowe, Guttman and Liskov asked for the weakest assumptions under which a protocol achieves a goal and left the question open. We answer it for assumptions about keys, values and channels. Call a run that violates the goal an attack, and the assumptions that would rule it out its stopping set. The least a protocol must trust to meet a goal is exactly the set of minimal ways to stop all of its minimal attacks. Several such sets may exist. The answer becomes unique once either/or assumptions are allowed, and it is a single set exactly when every minimal attack is stopped by a single assumption. A Galois connection between assumptions and goals explains why: a goal may end in "or", but its hypothesis may not. The same structure gives the trust needed by a conjunction of goals and an exact condition under which composed protocols need no extra trust. To compute the answer, a loop asks a verifier whether a candidate suffices, records what stops each attack it reports, and recomputes the candidates. Deciding whether some trust of at most k assumptions suffices is NP-hard. With a bounded analyser of our own and with CPSA, the loop finds the weakest trust for 18 goals over ten protocols and their variants, and on each it agrees with evaluating every trust using the same verifier. The answers include an assumption that our model of the adopted fix of Kerberos PKINIT states but the client's authentication of the server does not need, and channel assumptions under which Needham-Schroeder meets its goal in a bounded model.
