理论计算机科学电子笔记157（2006）61-78www.elsevier.com/locate/entcsGNDC模式罗伯托·戈列里a 法比奥·马蒂内利b Marinella PetrocchibaDipartimento di Scienzedellgorrieri@cs.unibo.itb意大利比萨研究中心信息和电信研究所fabio. iit.cnr.it，marinella. iit.cnr.it摘要我们在广义非演绎成分框架内正式定义了信用和责任的概念。我们通过文献中讨论的保留字：形式化方法，认证，广义不可演绎组合1概述形式化方法和工具已成功地应用于通信协议安全性的分析研究中的协议用给定的语言描述，然后定义要分析的安全属性的形式化规范。通过形式化分析协议在敌对环境中的安全性，即，考虑与诚实参与者并行运行的对手的存在。财产的正式规范和非正式定义都事实上，即使是一个常见的概念，如认证通常被认为是一个滑的安全属性（见[8]）。在安全社区中提出了几个Happiness，定义一个正式的1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.09.04062R. Gorrieri等人/理论计算机科学电子笔记157（2006）61认证模型是一项棘手的任务，实际上存在许多不同的形式主义[2，3，5，8，11，13，14，15]。他们的表现力，可用性和准确性经常受到质疑，例如[8]，一些专家致力于比较它们。在[4]中，比较了三种不同的认证属性，并且在广义非演绎成分模式（GNDC，[7，5]）中进行比较GNDC被提出来定义和分析安全属性，它基于不干涉的概念在本文中，我们试图正式捕获的两个不同的身份验证，信用和责任的含义。Abadi首先在[1]中将注意力集中在这两个属性上，讨论了认证消息m的两种可能用途假设主体A将消息发送给主体B。然后，就责任而言，此外，就信用而言，“B可以将m的信用归于A”。Abadi通过几个例子表达了信用和责任的概念，讨论了它们在协议设计和分析中的区别。不同的密码运算符（数字签名、加密、解密）可能导致责任或信用。我们的调查从阿巴迪的直觉开始，通过重新措辞：我们认为责任支持命令，即，代表某个当事人的公共消息，而信用与当事人有关，因为只有当事人事先知道秘密消息，秘密信息的持有者本文的结构如下。下一节回顾用于建模安全属性的GNDC模式。第3节定义了GNDC内的信用和责任第4节考虑了Abadi在[1]中分析的一些协议检查这些协议是否符合我们的正式定义。第5节提供了两个属性之间的正式比较的草图第六节是论文的感兴趣的读者可以在附录中找到2安全属性在本节中，我们介绍了[7，5]中给出的定义安全属性的通用模式GNDC。我们假设对进程代数有一定的了解。此外，在整篇论文中，我们通过Crypto-CCS指定协议和属性，[7]，基本上是用加密建模结构处理代数CCS。该语言的语法和语义可以在附录中找到。非正式地，GNDC模式规定系统规范P满足R. Gorrieri等人/理论计算机科学电子笔记157（2006）6163一C一CCCC一性质GNDCα（P），如果P的行为，尽管存在只能通过C中的一组通道与P相互作用的敌对环境Eφ，但似乎是相同的（w.r.t.观察等价的行为关系a）作为P的修改版本α（P）的行为，表示预期的P的正确行为。因此，GNDC模式具有以下形式P∈GNDCα（P）i ∈X∈ Eφ：（P<$X）\Ca α（P），（1）其中（P<$X）\C表示进程P和X的并行组合，仅限于通过C以外的通道进行通信。通过改变参数a和α，可以在GNDC模式中制定各种安全属性，[6]。在（1）中，在分析密码协议的特定上下文中需要一个额外的约束：敌对环境的静态（初始）知识必须绑定到一组特定的消息。这种限制是必要的，以避免一个过于强大的敌对环境，将能够破坏任何秘密（因为它将知道所有的加密密钥等）。形式上，Eφ代表所有通过通道进行通信的进程在C中，并且具有由φ约束的初始知识。我们认为只有属于Eφ的过程才是敌对过程。显然，在考虑到特定的形式框架（例如，类似CCS的进程代数）的情况下，（1）中的所有符号都需要被实例化。考虑一下这个例子α（P）≤痕量我的 <$X∈ Eφ：（P<$X）\C≤迹α（P）（2）关于GNDC在这里，迹包含关系已经被实例化为观察等价的被证明关系迹包含定义如下：我们说P的迹包含在Q的迹中（P≤迹Q）i，只要P可以通过一系列动作γ从状态P移动到状态PJ，那么Q也可以这样做，除了内部动作P和Q。迹包含关系是安全性分析的常用关系。当考虑≤trace时，存在用于静态表征的充分判据（即，不涉及GNDCα（P）的泛谓词[1]（更多细节见[7，5]）。3在GNDC架构中定义责任和信用根据Abadi [1]，他总结说，一些认证协议P∈GNDC64R. Gorrieri等人/理论计算机科学电子笔记157（2006）61适用于需要责任的申请，但不一定适用于需要信用的申请，反之亦然。因此，他声称需要更好地澄清认证协议的属性是否适用于建立责任和/或信用。我们相信，责任和信用可以类似于[15]中给出的对应属性的特征来定义（注意，在[11]中，对应被称为一致性，在CSP过程代数中被形式化，[13]）。在协议属性的描述中，技术上所做的是给每个主体执行控制操作的可能性，表达计算的当前局部视图。这些控制操作仅出于验证目的而插入到协议的规范中，并且主体在协议运行期间不能利用它们。请注意，使用对应操作以及协议操作之一被认为是指定和正确评估身份验证属性的良好机制（参见[9]）。3.1分配责任我们在这里正式定义责任财产。对于公共消息M1，对主体A承担责任指定M由A我们给出以下直观的解释属性：“A principal我们的非正式解释在日常生活中找到了它的动机，在那里，真正声称某事的人通常被认为对他所声称的负责。为了正式建模的财产，我们利用一对控制行动。我们定义了与接受责任和对称分配责任相对应的控制措施。我们将编写一个ccept resp（A，B，M），意思是该物业的详情如下：αAR（P）= α（x，y，m）∈D（P）acept resp（x，y，m）. assign resp（y，x，m）其中P是协议实例，D（P）是希望考虑的所有可能交付的集合。传递是三元组（x，y，m），其中x是发送者1公共消息是所有主体可能都知道的消息R. Gorrieri等人/理论计算机科学电子笔记157（2006）6165≤痕量消息m和y的接收者。αAR（P）在Crypto-CCS中指定。如果Q是代数中的一个项，则是ch（msg）。Q是在信道ch上发送消息msg然后表现为Q的进程。例3.1考虑一个协议实例P，其中有一个诚实用户A，一个恶意用户E和一个银行B。假设A（E）向B发送消息M（MJ），则集合D（P）为{（A，B，M），（E，B，MJ）}。我们在GNDC架构内制定责任如下：定义3.2P定义为分配资源的可能性P是GNDCαAR（P）。因此，一个协议在每次计算中都享有“责任”，在给予每个责任的行为之前都要接受这样的责任。我们注意到，由于我们考虑了基于跟踪的语义，在没有相应分配的情况下接受责任不被认为是攻击。3.2给予信贷我们在这里正式定义信用财产。将一条消息M的功劳归于委托人A，这表明A要求对一条特定的信息给予功劳简而言之，我们认为这个概念类似于只考虑秘密消息的责任。因此，我们对该性质给出以下直观解释：“A principal只有A最初知道M，并且A希望从B获得M的也就是说，为了从B那里得到信任，A应该让B相信消息M是由A自己拥有的。举个例子，假设B统治着一个科学委员会，A是一位科学家，他发现了一种迄今为止被认为难以治愈的疾病的治疗方法。因此，A向B发送了一条消息，其含义可以大致表示为：所述治疗是Y.我需要这样一个发现的父亲。首先，B应该验证消息来自A，并且实际上是由A发起的。A.B.A. B. C. D. D. D. C. D. B应该为医疗发现提供A的亲子关系）。Y可以是B事先不知道的东西，但B可以很容易地验证它。再举一个例子，假设B确实统治了一个智力竞赛节目。某个外部可信的第三方，例如公证人，可以事先将正确答案的摘要提供给B 在收到来自A的答案后，2当一个消息不为协议中除A之外的其他主体所知时，该消息对于主体A来说是秘密的。66R. Gorrieri等人/理论计算机科学电子笔记157（2006）61≤痕量一B通过比较两个字母来验证它的正确性。如果它们相等，B可以把答案归功于A为了对信用属性进行正式建模，我们引入了一对新的控制动作。我们用行为ask cre表示A对B的信用请求，用行为giveive cre表示信用给予。协议应确保B仅在A要求时才给予A信贷。该要求通过以下规范来实现αGC（P）= α（x，y，m）∈D（P）ask cre（x，y，m）. giveive cre（y，x，m）集合D（P）的一个特殊特征在上面的信用性质定义中是至关重要的关于第3.1小节中给出的责任定义，我们对D（P）施加了一个约束，以模拟我们不考虑公共价值的事实。我们假设在D（P）中不可能有两个（或更多）具有相同消息m的三元组。通过这个约束，我们假设只有一个主体能够为某个消息请求信用我们称这个假设为在对协议建模时，我们通常只描述运行协议的诚实代理。然而，在该特定框架中，正确递送的集合D（P）还应当考虑可能的恶意用户的递送。特别是，这种交付必须考虑属于恶意用户的知识的每个可能的消息（并且除了其他用户的私有消息）。我们把这个假设定义3.3假设D（P）满足消息唯一性条件和正确发送能力条件。那么，P满足给予信贷iP是GNDCαGC（P）。在轨迹方面，如果给定cre（B，A，M）的动作存在于轨迹中，则动作skcre（A，B，M）必须先前在同一轨迹内发生在下面的部分中，我们考虑了阿巴迪在[1]中分析的一些协议，并检查这些协议是否符合我们对信用和责任的正式定义。4示例4.1第一示例[1]中分析的第一个协议展示了如何从主体A向主体B发送短期公钥K（消息1）。短期公钥使用主体A的长期私钥K-1签名。T是时间戳。R. Gorrieri等人/理论计算机科学电子笔记157（2006）61671B一KKKA（m，k）d=ef[k，A，B，T），k−1x] ask cre（A，B，m）.AEncc1（（A，B），x）. [m，k−1cy][y，kBcz]c2（（A，B），z）B（k）d=efc（y）。[y]snd z][z，k][z，k][z，k]t][tFST[u][ u]snd b][b=B][u][美国][rsnda][rfstkJ]c2（w）. [wsndh][h，k−1decj]给定cre（b，a，g）Pd=efA（M，K）<$B（K）表1第一示例然后，短期秘密密钥K-1被用于后续消息（例如，消息2）用于签署另外的消息，例如，M.该协议假设B知道A消息1A→B：A，B，{K，A，B，T}−1一Message2A→B：A，B，{{M}K−1}KB就信用而言，我们想知道下面对消息1的解释是否正确：主体A要求主体B对用K-1签名的消息给予信用。在Tab。1，协议在我们的进程代数中表示。适时地插入期望的控制动作ask cre和giveive cre我们要求主体A实际上拥有M，以防止中间人攻击。事实上，让我们考虑[1]中提出的攻击（攻击者的行为在Tab中正式定义。（2）：消息1A→E（B）：A，B，{K，A，B，T}−1一消息1EMessage2A→E（B）：A，B，{{M}K−1}KBMessage2我们将伪装成B的攻击者表示为E（B）。攻击者拦截从A到B的消息，用自己的消息替换它们。在消息1'和2'中，攻击者冒充自己。特别地，E使用K提出信用请求，因此E可以从A实际上，当B从E接收到消息1（E，而不是A，实际上是在和B说话）。在实践中，E的行为很糟糕，68R. Gorrieri等人/理论计算机科学电子笔记157（2006）61KB≤痕量Ed=efc1（x）[x=sndy]% E拦截A的消息1[y，kAdecz]% E解密{K，A，B，T}-1和一[nz，k−1nnw]% E在K−1E Ec1（（E，B），w）.%E将A替换为E并发送c2（j）。[jfstk]%E截取sAc2（（E，B），k）%用E代替A。 然后发送到B%themessageE，B，{{M}K−1}KB表2第一个例子是信用攻击消息，但然后它正确地执行协议的步骤，这是一个小精灵的角色。 注意Ecnnotdecryptmessage{{M}K−1}KB，因为它不知道K−1。因此，E不拥有M。让我们来看看这个过程PJ=。（PE）\ {c1，c2}，c1andc2作为分别在其上交换消息1，1'和2，2'的信道那里存在这个过程的一个迹，它不是αGC（P）的迹。事实上，如果上述攻击成功发起，我们可以在PJ中找到一个迹，其中给定cre（B，E，M）动作之前是一个sk cre（A，B，M）动作。因此，即使A先前已经要求对消息M的信用，B也可以对消息M的信用给予E 相反，考虑到对D（P）的限制，我们不能有两个与处理同一消息的交付有关的信用请求，即，A B M和E BM因此，我们不能有一个迹，其中给定cre（B，E，M）在αGC（P）中的sk cre（A，B，M）之后执行因此，P∈/G NDCαGC（P）. 因此，我们得出结论，足以给予信贷。我们相信，责任与公共信息有关，就像信息{M}K-1与KB 的关系一样。因此，它将增强E对它发送给B的消息的责任感。不幸的是，我们对责任的形式化并不符合阿巴迪这在形式上在于以下事实：A发出accept resp（A，B，M）动作（表1中的消息m必须被适当地实例化），而B必须执行assignresp（B，E，M）（同样，具有表1中的变量的适当实例）。通过允许攻击者发布控制行动，许多明显的针对责任的攻击将消失。如果R. Gorrieri等人/理论计算机科学电子笔记157（2006）6169RX，ARRX，ARγ代理E在发出控制动作时行为正确，则E发出动作acept resp（E，B，M），并建立与控制动作asign resp（B，E，M）的对应关系。我们要求对手以公平的方式发出控制动作每当对手作为诚实的参与者时，它就会发出相应的控制动作。请注意，与以前的文献相反，这里我们允许对手输出控制动作。因此，我们放宽了GNDC的要求，即对手只能通过一组通道C进行交互。在这里，我们还允许对手在特殊的控制通道上输出控制动作，仅用于验证目的。基本上，我们增加了对手可以做的动作。为此，我们引入算子↓Xs. t.， 给定一个并行系统S和一个顺序过程X，如果则γ↓X表示X在计算γ。假设对手可以作为恶意用户或诚实用户。然后，它的诚实行为由规定其角色的进程RX（这是Crypto-CCS术语）描述RX代表X的角色。我们定义谓词HonX（γ），它告诉我们X的行为是否正确w.r.t.控制动作。非正式地说，X在w.r.t. 因此，无论何时执行其角色的第一动作，该第一动作之前已经有适当的第一动作3。当恶意代理只能执行接受响应控制操作时，谓词HonX（γ）可以定义如下：XRX，AR我的（γ）⎛X = α1. αn⎜埃西体育馆⎞⎟⎟→α=accept resp（X，y，m）你好。2≤j≤n：αj=FST（RX，y，m）j−1⎝ ⎠m∈ D（φ <$msgs（α1，. ，αj−1））其中FST（RX，y，m）是X在计算γ期间执行的第一个动作，遵循其角色RX并涉及接收者y和消息m。一个进程可以发布一个包含某个消息的控制动作，只有当这个消息属于它在序列α1，. ，αj−1。这3没有必要研究恶意用户在协议中作为响应者的正确行为，因为缺少ssign resp动作并不重要。议员70R. Gorrieri等人/理论计算机科学电子笔记157（2006）61≤R，ARRX，GC≤R，GC这一要求对于我们对信用和责任的不同描述是至关重要的。广义上讲，我们的想法如下。第三方可以被认为对它实际发送的某些公共消息负责，但是，当它根据中间人方案行事时，它不能具有任何分配用于转发它实际上不知道的消息的信用。我们定义了一个过程之间的关系，它是经典迹包含关系的一个细化。定义4.1当概率≤RX时，AR的定义如下：S≤Sγi {γ|SX（γ）}{γ |Sγ1RX、AR21=RX，AR中的ΔH2=0}因此，GNDC架构中的责任最终可以定义为：定义4.2PsatisfiessAssigningResponsibilityyP是G NDCαAR（P）。X同样，我们可以定义谓词HonX一个关系≤RX，GC用于信贷资产定义4.3假设D（P）满足消息唯一性条件和正确发送能力条件。那么，P满足给予信贷iP是GNDCαGC（P）。X这些略有不同的概念使我们能够识别出正确遵循协议步骤的可能让我们再考虑一下中间人攻击，在这种攻击中，敌人在向B发送信息的同时扮演自己的角色。现在E可以发出控制操作。由于消息2中的加密通信防止学习消息M，并且由于对D（P）的限制，仍然存在信用攻击（E确实不被允许为它不知道的消息请求相反，E不再是一个谈论责任的敌对攻击者实际上，由于M被假设为公共消息，因此E可以发出控制动作ccept resp（E，B，M）。此操作与B引发的相应assign resp（B，E，M）匹配。因此，没有责任攻击。我们后一种信用和责任的形式化与阿巴迪在[1]中提供的直觉一致4.2二示例在阿巴迪的第二个例子中消息在B的公钥KB下加密会话密钥然后可以用于进一步的消息（例如，消息2和3）。该方案具体如下：R. Gorrieri等人/理论计算机科学电子笔记157（2006）6171消息1A→B：{A，K}KB消息2A→B：{M}K消息3B→A： {MJ}K我们同意阿巴迪只有B可以从消息1中检索K，那么A可以合理地让B对K下加密的消息负责（除非A本身没有生成加密的消息）。该协议假设两个主体都可以识别它们自己的消息）。我们还注意到，消息1中A的身份的出现相反，B不能让A对在K下加密的消息负责，因为消息1可以由其他人假装是A生成。实际上，来自B的asign resp（A，B，MJ）动作的可能问题将永远不会是前面是来自A的对应者acept resp（B，A，MJ）的发布。让我们考虑一下信贷资产。阿巴迪认为，这个协议似乎给了A一种“无资格”的通过在消息1中包括它的名字，A可以要求对在K下加密的消息的信用。现在假设A不合格地或恶意地选择了K。 在这种情况下，第三方C可以发送消息{MJJ}K到B。因此，C给出了A为M留言该这种情况与我们的直觉相反，我们的直觉认为，某些人给我们的信息必须是我们自己有意识地发送的。根据我们对信贷的定义，委托人仅可因其能够履行的“要求信贷”行为而获得信贷。因此，我们排除了“无条件”信贷的优惠形式。从形式上讲，很容易验证所研究的协议并不保证A的信用。由于消息1不提供A然而，如果A不具有M，则A不能发出控制动作ask cre（A，B，M）。在这种情况下，将存在给定cre（B，A，M）的动作，而不是对应的sk cre动作，因此，信用攻击。4.3三示例在他的论文中，Abadi给出了第三个例子，一个用作Krawczyk的SKEME协议的组件的协议该协议的目的是从两个随机量（JA和JB），主体A和主体B分别发明的共享密钥。A和B互相发送这些随机数，用接收方的公钥他们最终计算出一个共享的72R. Gorrieri等人/理论计算机科学电子笔记157（2006）61通过将单向散列函数应用于JA和JB的级联来计算密钥K。共享密钥可以在A和B之间的后续通信中使用。年龄1A→B：{JA}KBMesage2B→A：{JB}KAK=H（JA，JB）让我们考虑以下在线攻击：MESS 年 龄 1A→B ：{JA}KBMessage1B→C ：{JA}KCMess 年 龄 2C→A ：{JC }在这种情况下，A与恶意主体B一起发起协议，恶意主体B将AA和C都计算了相同的共享密钥K（K不会被B知道），但是A错误地认为它与B共享K，而C认为它与A共享K。这种攻击假设B使C相信消息1此外，A认为消息2来自B。根据这个计算，C可以对在K下加密的消息向A主张信用。这就导致了信用攻击。假设通信分别在信道cab、cbc和cca上进行，并考虑PJ=. （A<$B<$C）\{c，c，c}. 如果我们的肛门是从w或k开始，我们可以ab bc ca在P's观察到动作ask cre（C，A，MJ）（假设C拥有M同样，对B也有责任攻击。事实上，来自C的每个消息将被分配给B（即，A可能认为该消息得到B然而，由于B行为恶劣，我们是否必须研究对B的责任攻击是值得怀疑的。当B作为一个例子，考虑C发送的消息包含输入C的秘密数据的密码的情况A可能相信这样的凭证是由B从C发送到A的消息可以是因此，在我们的解释中，我们对响应者进行了信用和责任攻击。5比较非正式地说，在分析前面的例子时，似乎给予信贷至少和分配责任一样困难。特别是，如果我们R. Gorrieri等人/理论计算机科学电子笔记157（2006）6173MP≤R，GC限制为仅考虑过程s. t上的AR。D（P）对信用有限制，那么显然这两个概念是相等的。事实上，我们对信用的定义可以被想象为一种责任要求，只要我们要求责任的信息是秘密的。GNDC分析框架适用于形式上比较不同的安全属性。实际上，由于责任是为公共信息定义的，而信用是为秘密信息定义的，因此不可能对这两种属性进行正式的比较。为了使其可行，我们需要放弃关于信用规范中消息保密性虽然与以前的提法保持一致，但另一种定性可以是：我们有一个信用攻击，每当用户B给信用A的消息M，要么A没有要求信用从B的消息，或有另一个用户C谁要求信用从B的M之前，A。这表达了请求信贷的竞争条件的一种形式。提供了一个正确的环境，每当用户愿意要求信贷的消息M，M应该只知道自己4。因此，如果协议是正确的，没有其他人可以尝试为该消息请求信用粗略地说，这意味着如果一个协议满足我们以前对信用的定义，那么它也满足当前的定义。上述特征没有提到秘密值。一种可能的正式化方式如下：jm=（x，y，m）∈D（P）mask cre（x，y，m）.（给出cre（y，x，m）。<$（<$（xJ，yJ，m）∈D（P）\{（x，y，m）}askcre（xJ，yJ，m）αGC J（P）=Jm∈MDm其中MD={m|（x，y，m）∈D（P）}是D（P）中所有可能出现的消息，D（P）m={（x，y，m）∈D（P）}是D（P）中包含消息m的三元组。给定一个消息m，只有第一个请求m的信用将被服务。定义5.1P定义GivivinggCred i t itE为G NDCαGCJ（P）。X我们现在可以与责任属性进行比较。4.在特殊情况下，我们也可以允许接受者知道M。 更有可能的是，接收者可以简单地有一种方法来验证消息，例如通过具有消息摘要。P74R. Gorrieri等人/理论计算机科学电子笔记157（2006）61命题5.2如果P享有信用（定义5.1），则P[f]享有责任（定义4.2），其中f（ask cre）= acccept resp，f（give cre）= assignresp。基本上，证明是通过注意到，直到重命名的行动，f，则有αGCj（P）≤traceαAR（P）.6结论我们已经在一个良好建立的模式中定义了信用和责任属性的可能概念，用于建模和分析安全属性。我们还考虑了阿巴迪分析的一些协议，[1] 我们检查了这些协议是否符合我们的正式定义。我们已经粗略地对这两种性质作了形式上的比较。我们的结论是，我们对信用和责任的定义几乎总是遵循阿巴迪然而，正如我们的研究所强调的那样，我们认为信用应该被认为是比责任更强的财产，而[1]给出了一些特殊情况，这似乎并不完全合理。事实上，目前的工作和[1]中的工作对“无条件信贷”的概念进行了区分 Abadi允许用户C代表用户A发言。作为因此，A可以因为A没有做过的陈述而得到信任。相反，我们强制用户A只为自己发出的消息获得信用。这两个性质的某些方面已被横向处理。事实上，我们也将我们的定义投入工作，并让它们为[12]中数字证书的安全发布读者应该注意到，本文所给出的只是对这两个性质的一种可能的解释。因此，可以启动进一步的研究，以调查这些性质的其他假设是否与阿巴迪的直觉相一致我们注意到，这里的选择很可能是任意的，可以遵循其他方向。作为未来的工作，我们的目标是继续这些调查，由于相关的治疗主题。最后，我们实际上处理的是直接责任和直接信贷，而不是授权。在我们的（和其他）框架中，如何解释授权是值得研究的。确认我们要感谢匿名推荐人提供的有用意见。这项工作得到了欧盟FET项目“面向服务的覆盖计算机软件工程（SENSORIA）”的部分支持R. Gorrieri等人/理论计算机科学电子笔记157（2006）6175引用[1] Abadi，M.，身份验证的两个方面，CSFW'98会议录[2] Abadi，M.，Security Protocols and Specifications，Proc. of FOSSACS[3] Burrows，M.，Abadi，M.，和Needham，R.，认证逻辑，技术报告39，1989，DEC系统研究中心。[4] Focardi，R，Gorrieri和Martinelli，F.，A Comparison of Three AuthenticationProperties，TCS291，3（2003），285-327.[5] Focardi，R和Martinelli，F.，A Uniform Approach for the Definition of Security Properties，Proc. of FM[6] Focardi，R，Gorrieri和Martinelli，F.，安全属性的分类-[7] Focardi，R，Gorrieri和Martinelli，F.，密码协议分析的非干扰性，Proc. of ICALP[8] Gollman，D.，On the Verification of Cryptographic Protocols - A Tale of Two Committees，Electronic Notes in Theoretical Computer Science32（2000）.[9] Gollmann，D.，安全方面。Proc. of Global Computing'03，Springer，2003，LNCS 2874，192-202。[10] Krawczyk，H.，一种安全的因特网密钥交换机制，1996年国际互联网安全会议论文集[11] Lowe，G.，一种认证规范的层次结构，Proc. of CSCW[12] Martinelli，F.，Petrocchi，M.，Vaccarelli，A.，A Formal Analysis of Two SecureProcedures for Certification Delivery，接受出版STVR16，1（2006）。[13] 瑞安，P.，施耐德，S.，戈德史密斯，M.，Lowe，G.，Roscoe，B.，安全协议的建模和分析：CSP方法，Addison-Wesley，2000年。[14] Thayer J.，赫尔佐格·J和Guttman，J.，串空间上的诚实理想，Proc. of CSCW[15] T.Y.C.和Lam，S.，一种用于认证协议的语义模型，Proc.of SS一种加密CCS该语言的模型由能够通过交换消息进行通信的顺序代理该语言的数据处理部分由消息和推理系统组成消息是由代理操作的数据，它们形成一组可能包含变量的术语Msgs集合Msgs由语法定义m：：= x|B|F1（m1， . . . 、mk1）|.... . . 你 好 。 . |F1（m1， . . 、m、k、l）其中Fi（1≤i≤l）是消息的构造函数，x∈V是可数变量集，b∈B是基本消息的集合，ki，对于76R. Gorrieri等人/理论计算机科学电子笔记157（2006）61n1≤i≤l，给出构造函数Fi的参数个数。没有变量的消息是封闭消息。推理系统对消息上可能的操作进行建模。它们由一组规则r组成，例如， ：r= m1.. .Mn米0其中{m1，. ，mn}是前提的集合（可能是空的），并且m0是结论。将规则r应用于已关闭消息mi的实例表示为m1 ...mnrm0. 给定一个推理系统，定义一个演绎函数D，使得如果φ是封闭消息的有限集合，则D（φ）是可以通过应用系统中的规则的实例从φ开始推导的封闭消息的集合。Crypto-CCS的语法和语义相对于给定的推理系统是参数化的。实例推理适合于对特定密码协议建模的系统将在以下部分中示出。语言的控制部分由复合系统组成，即，并行运行的顺序代理。语言语法如下：复合系统：S：：=（S1<$S2）|S\C|A φA：：=0|p. 一|A1+A2|[m1.. . mnrx]A1;A2| [m = mJ] A1 ; A2 | E(m1,...,米）的P重定位构造：p：：=c！M|c？X其中，m，M，m1，. ，mn是封闭消息或变量，x是变量，c ∈Ch（通道的有限集合）φ是封闭消息的有限集合，C是Ch的子集。0是什么都不做的进程。p. A是一个进程，它可以根据特定的前缀构造p执行一个动作，然后表现为A。特别是• c！m表示在信道c上发送的消息m;• c？X表示在信道C上接收消息M。接收到的消息替换变量x。A1+A2表示A和A1之间的非确定性选择。[m1. . . mnrx]A1;A2是一个非线性结构。 如果，以规则r为例，前提是m1.mn，则可以推断出消息m，则进程表现为A1（其中m替换x），否则表现为A2。[m=mJ]A1;A2是一个用于计算等式的结构。 如果m=mJ则系统表现为A1，否则表现为A2。复合系统S1<$S2表示S1和S2的并行执行。如果S1和S2中的一个子组件执行p，则S1和S2执行动作p。一个同步，或内部行动，表示为τ，可能会发生，每当R. Gorrieri等人/理论计算机科学电子笔记157（2006）6177−→}a∈Act′一′1′φφ−→φ−→φ1 φa'（）S−→S1a′（！）SS1−→SS1c！Mc！m′c？M′（c！m.A）φ−→（A）φ（）S−→S S1−→S12τ′ ′（？）m∈MsgsSS1−→SS1c？Mc！m′（c？x.A）φ−→（A[m/x]）φ<${m}（\1）S−→Sc∈/La'c！m′m1. . . mn<$rm（A[m/x]）φ<${m}−→（A）φ'S\L−→S\L（D）a'a'（[m1. mn<$rx] A; A1）φ−→（A）φ（+2）S−→SS+S1−→S′/ms.t. m1... mma'（D1）nr（A）−→（A1）φ一'（[m1. mn<$rx] A; A1）φ−→（A1）φ（=） m=m′（A）a（A）“'a''（[m=m]A;A1）φ−→（A）φ（=1） m m′（A）a（A1）““a"（[m=m]A;A1）φ−→（A1）φE（x1，.，x）=11a1（常量）ndefA A[m /x，.，mn/xn] −→A一E（m1，.，mn）−→A1图A.1. Crypto-CCS的操作语义S1和S2能够执行两个互补的动作，即，在同一信道上发送复合系统S\C只允许通道不在C中的可见动作。（内部作用τ是看不见的作用）。术语Aφ是一个单一的顺序代理人，其知识，即，在其术语中出现的消息集合由φ描述。代理人的知识增加时，它收到的消息（见规则（？）（见图A.1中的规则D）或从已知的消息中推断新的消息。对于每一个序列智能体Aφ，要求出现在Aφ中的所有封闭消息都属于它的知识φ。代理的活动由它们可以执行的操作描述。复合系统可以执行的动作的集合Act的范围为a，并且它被定义为：Act={c？m，c！m，τ |c ∈ C，m∈Msgs，m闭}. P是所有Crypto-CCS封闭项的集合（即，没有自由变量）。sort（P）是在术语P中语法上出现的所有通道的集合。Crypto-CCS术语的操作语义通过以下方式来描述：标记跃迁系统（简称lts）的α P，α t，{a在哪里？{−→a }a∈Act 是Crypto-CCS进程之间的最小关系，′′78R. Gorrieri等人/理论计算机科学电子笔记157（2006）61−→公司简介图的公理和推理规则A.1（在该图中，1，S−→aSJ的表达式意味着系统可以从状态S通过动作a变为状态SJ。表达式S=SJde-注意到S和SJ属于τ的自反传递闭包;γ设γ = a1. an∈（Act\{τ}）n是动作序列。那么，S=J，如果S=a1anJ−→= =−→=S。
我的内容管理
展开
