量化普适认证：Hancke-Kuhn协议的案例
Quantifying pervasive authentication: the case of the Hancke-Kuhn protocol
摘要：
随着移动设备遍布物理空间，熟悉的认证模式变得不足：除了实体认证之外，许多应用需要，例如，位置认证。许多有趣的协议已经被提出和实现，以提供这种加强形式的认证，但很少有证据表明，这样的协议满足所需的安全属性。逻辑形式主义，设计用于推理标准计算机网络上的安全协议，原来是难以适应推理的混合协议，用于普及和异构网络。<p>我们完善的Dolev-Yao式的代数方法的协议分析的概率模型的猜测，需要分析的协议，混合弱密码学与非标准的通信信道的物理特性。应用这个模型，我们提供了一个精确的安全性证明的邻近认证协议，由于Hancke和库恩，使用一种微妙的形式的概率推理，以实现其目标。
英文摘要：
As mobile devices pervade physical space, the familiar authentication patterns are becoming insufficient: besides entity authentication, many applications require, e.g., location authentication. Many interesting protocols have been proposed and implemented to provide such strengthened forms of authentication, but there are very few proofs that such protocols satisfy the required security properties. The logical formalisms, devised for reasoning about security protocols on standard computer networks, turn out to be difficult to adapt for reasoning about hybrid protocols, used in pervasive and heterogenous networks. <p> We refine the Dolev-Yao-style algebraic method for protocol analysis by a probabilistic model of guessing, needed to analyze protocols that mix weak cryptography with physical properties of nonstandard communication channels. Applying this model, we provide a precise security proof for a proximity authentication protocol, due to Hancke and Kuhn, that uses a subtle form of probabilistic reasoning to achieve its goals.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
