基于互模拟的非确定性干扰在密码协议中的应用

网址：http://www.elsevier.nl/locate/entcs/volume61.html24页基于互模拟的非确定性容许干扰及其在密码协议圣伊法内拉弗朗斯1;2约翰马林斯1;3，部门。计算机和软件工程Ecole Polytechnique de Montr eal蒙特利尔，加拿大摘要本文首先定义了一个基于互模拟的非确定性容许干扰（BNAI），导出了它的过程论特征，并给出了一个关于通信过程上主算子的组合验证方法，从而将文[19 ]中基于迹的类似结果推广到基于观测的互模拟的新概念[6]。与其基于跟踪的版本一样，BNAI仅通过降级器（例如密码系统）承认信息在保密级别之间流动，但被措辞为观测等价性的概括[18]。然后，我们描述了一个可接受的干扰为基础的方法来分析密码协议，扩展，在一个非平凡的方式，在[11]中提出的非干扰为基础的方法。用BNAI定义了密码协议的一致性和认证性，并给出了它们各自的基于互模拟的证明方法。最后，作为该方法的重要说明，我们考虑简单的案例研究：宽口青蛙协议[1]和Woo和Lam单向认证协议[25]的典型示例。这种方法的最初想法是证明入侵者可能干扰协议，只有通过选定的信道被认为是允许的，当导致无害的干扰。1引言系统分析中的一个基本问题是确保程序不会将敏感数据泄露给第三方，无论是恶意的还是无意的。1 第一作者得到了NSERC研究生奖学金的支持，第二作者得到了加拿大政府NSERC资助号138321-01的支持。2 电子邮件：stephane.lafran ce @po ly mtl. CA3 电子邮件：John.Mullins@po ly mtl. CAc 2002年由Elsevier Science B出版。诉 在CC BY-NC-ND许可下开放访问。2安全问题的这一关键方面通常被称为保密。信息流分析通过澄清程序中的信息流是安全的（即高级信息永远不会流入低级通道）的条件来解决这一问题。这些条件称为非干扰属性[10]，捕获高级动作和低级行为之间的任何因果依赖关系。然而，许多实际的保密问题超出了不干涉的范围。例如，密码系统允许加密的私有或分类信息安全地流到未受保护的（即低级）信道上，而不管一方面秘密数据m和加密密钥K与另一方面解密数据fmgK（m由K加密）之间的明显因果依赖性。实际上，m或K的任何变化都反映在fmgK中。 在这种情况下，主要关注的是确保程序只通过密码系统或更一般地通过降级系统泄漏敏感信息。容许干扰[19]就是这样一种性质。在本文中，我们定义了一个基于互模拟的语义的非确定性容许干扰。看来，基于观测cri-0或O-互模拟（在[6]中称为O-同余）的观测依赖互模拟为表达基于互模拟的非确定性允许干扰（BNAI）提供了合适的理论框架正如我们将看到的，BNAI具有优雅的过程理论表征（传统上称为信息流理论中的解旋定理）和有吸引力的组合性属性。已经设计了基于非干扰的方法来分析密码协议[12，9]。该方法的基本思想是证明没有入侵者可以干扰协议。在本文中，我们考虑到加密所引起的干扰是可容许的，从而改进了这种方法。这种可容许的干扰可以通过简单地识别与协议中发生的加密动作相对应的降级动作来表示。本文将突出两种优势的容许干扰为基础的方法比非干扰为基础的。在某些情况下，该方法允许分析协议的信息流，而不需要用加密和解密运算符扩展进程代数的syn- tax。在其他情况下，它允许在规范级别丢弃无害干扰，即不对应于成功攻击的干扰，而不是从验证过程的副产品中手动筛选本文的结构如下。在第2节中介绍了一个变体的值传递CCS，扩展了Boudol的观察准则及其基于观察的双模拟语义。第3节介绍了基于观测依赖互模拟的非确定性容许干扰及其代数过程特征和与主要过程算子的相容性。在第4节中，我们提出了不同的方法来使用BNAI在密码协议的分析。更具体地说，我们专注于配置和身份验证属性。这些属性是根据BNAI和它们各自的互模拟来定义的3的证明方法。通过第5节中的Wide Mounted Frog协议和第6节中的Woo和Lam单向认证协议进一步研究了该方法。我们在第7节中总结了相关的和未来的工作。2预赛2.1传值CCS我们需要通过确定一种计算语法来开始讨论，以构建调查。我们的工作是基于价值传递CCS[18]，随着我们的前进，它会以各种方式进行修改我们考虑以下消息代数，其项由a表示，定义为：a ： =v （ value ） j x （ variable ） j （ a; a ） （ pair ） j faga（encryption）：我们将fv（a）表示为a中出现的（自由）变量的集合，当fv（a）= ;时，我们说a是闭项。在本文中，任何闭加密项fa1ga2都被看作是以闭项a2为密钥加密闭项a1所得到的原子值。对于任何（原子）值v和x 2 fv（a），我们写a[v=x]来表示a中x的每次出现都设置为值v，a[v1 =x1][v2 =x2]记为a[v1 =x1; v2 =x2]，依此类推。此外，我们假设一组至多可数的通道，范围由c。每channel是有类型的，即具有可以在其上发送和接收的术语（消息）的唯一结构。我们写dom（c）来表示可以沿着c携带的术语的域。我们的扩展值传递CCS的动作，范围为，是从一个通道和一个项的组合中获得的，如下所示：c（a）或c（a）（输出动作），c（a）（输入动作），（内部行动）。对于任何a2 dom（c）。因此，Act = V is [f g]的集合包含可见动作Vis = In[Out]的集合，其中In是输入动作的集合，Out = In是输出动作的集合，并且函数[：]：V is！V是这样的=。我们定义一个动作的自由变量的集合，用fv（）表示，作为集合fv（a），如果= c（a）或= c（a），fv（）=;如果= . 我们说一个动作如果fv（）= ;，则它是封闭的，否则我们说它是开放的，我们使用到在封闭操作的集合上的范围。代理（由P和Q组成）的构造如下：0（空代理）;：P（pre x）;int n = nums（nums）;4P + Q（总和）;5嗨Lo