共享密钥认证协议的安全性分析

理论计算机科学电子笔记99（2004）267-293www.elsevier.com/locate/entcs工作中的E-spi演算：身份验证案例研究Riccardo Focardia，1，2 Matteo Maffeia，1，3a意大利威尼斯Ca'Foscari大学信息学系摘要在文献[10]中，我们引入了一个描述安全协议的进程演算，并提出了实体认证的静态和组合分析。在本文中，我们应用这样的技术在著名的共享密钥认证协议。分析有助于澄清协议逻辑，建议简化和揭示一些攻击。此外，我们将讨论我们的分析如何扩展到多协议系统。保留字： 安全，进程演算，静态分析1介绍安全协议被设计为在可能敌对的环境中提供各种安全保证：典型的保证包括两个可信实体之间的消息交换的保密性，消息的新鲜性和真实性，声明身份的真实性，...... 和更多.恶意实体的存在使得协议设计复杂并且经常容易出错，如文献中报道的对长期协议的许多攻击所示（例如，[12、15、20、22、25、27]）。在大多数情况下，这种攻击都集中在协议1由MIUR项目“Modelli formali per la sicurezza”和欧盟合同IST-2001-32617“移动分布式系统安全性的模型和类型”（MyThS）部分支持的工作2 电子邮件地址：focardi@dsi.unive.it3 电子邮件地址：maffei@dsi.unive.it1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.02.012268R. Focardi，M. Maffei / Electronic Notes in Theoretical Computer Science 99（2004）267-事实上，即使假设密码学是完全可靠的构建块，入侵者也可以采取许多潜在的危险行为，特别是拦截/重放/伪造消息，以破坏预期的协议不变量。形式化方法作为协议设计和验证的工具已经被证明是非常成功的。一方面，针对正式规范的模型检查协议的失败已经导致了几种攻击的发现（例如，[22、23、24、26、27]）。另一方面，基于类型系统和控制流分析的静态技术已被证明可以有效地为协议的正确性提供静态保证概述静态分析也是我们在[10，9]中提出的技术的基础：我们制定了一组关于协议执行的可判定条件，这些条件意味着对一大类协议的分析是在每个参与者上孤立进行的：每个经过验证的主体都被判定为本地正确。我们的主要结果是，由本地正确的主体组成的协议是安全的，即，顺从的和经验证的主体的任何组合对由任何协议入侵者4发起的攻击是免疫的。我们的技术基于一种新的过程演算，称为spi-spi演算，我们使用它来指定感兴趣的认证协议：spi-spi演算是spi演算的方言[4]，包括一组受协议叙述过程演算Lysa[6]启发的特定于认证的结构在本文中，我们将上述技术应用于一些众所周知的协议：Iso对称密钥两次通过单边认证协议[21]，基于nonce的版本的宽口青蛙协议[4]，Woo和Lam认证协议[29]和修正的Needham Schroeder共享密钥协议[28]。我们的目的是表明，分析是适用于广泛的认证协议。基于我们的分析，我们证明了安全的正确的协议的无限数量的会话，在某些情况下，我们提出了简化。另一方面，我们的分析未能验证可能存在攻击的有缺陷的此外，我们表明，我们的分析有助于澄清和形式化的协议背后的逻辑。我们还给出了一个多协议系统的例子，其中实体运行不同协议的多个会话。我们分析了不同会话之间的交织，并讨论了我们的分析如何保证其安全性。论文的结构 § 2给出了一个简短的概述，spi-spi演算和它的操作语义。§3总结了我们的静态分析及其主要属性。第4节介绍了一些案例研究。在§5中，我们给出了一个多协议系统的例子，在§6中，[4]我们隐含地诉诸标准的Dolev-Yao入侵者模型[14]。入侵者可以拦截、回复和伪造新的消息，但在不知道相应密钥的情况下永远不会解密消息。R. Focardi，M. Maffei / Electronic Notes in Theoretical Computer Science 99（2004）267-269一些总结性的评论。2spi演算Spi演算衍生自Spi演算[4]，并继承了Lysa的许多特征，Lysa是[6]中提出的用于分析认证协议的Spi演算的一个版本在以下几个方面，Escher-spi演算与这两种演算不同（i）它结合了来自[9]的标记消息交换的概念，（ii）它提供了用于声明进程身份和（共享的）长期密钥的原语，（iii）它提供了新的有用的认证特定构造。表1.符号：d在简单名称和简单变量上的范围，I在标识标签上，A，B在主标签上，TTP标签上的T，标签上的C：{Claim，Owner，Verif，Key，Id}，D：：=数据n个简单的名字n：C标签名称x简单变量x：C标记变量P，Q：：=过程IdS（principal）我愿意！S（复制）P|Q（组成）设k= key（I1，I2）. P（Key Assignment）S：：=顺序过程0（无）在（D1，...， D m）。S（输入）out（D1，.， D m）。S（输出）新的，新的。S（限制）将 x 解 密 为 {D1 ， ... ， Dm}d 。 S（decryption）encrypt{D1，.，Dm}d作为x 。 S （ 加 密 ） 运 行 （ I1 ， I2 ） 。 S（运行）（I1，I2）. S（commit）语法. 演算的语法如表1所示。我们预先假设两个可数集：N，名称和V的变量。我们保留a，b，k，m，n作为名字，x，y，z作为变量。名称和变量都可以被标记，分别标记为n：C和x：C。标签是一种特殊的名称类别，包括角色（三个特殊名称Claim、Owner、Verif）、身份标签Id和会话密钥标签Key（标签在第3节中解释，它们的使用在第4节中说明）。身份ID是名称的子集，ID_ID_N，其被进一步划分为主体IP和可信第三方（TTP）IT。进程（或协议），范围由P，Q形成的并行组合，可能复制，顺序进程，范围由S。流程形式IdS表示代表某个实体运行的顺序流程S270R. Focardi，M. Maffei / Electronic Notes in Theoretical Computer Science 99（2004）267-由I识别。一个顺序进程永远不会分叉成两个并行进程。这个假设有助于将ID中的唯一身份分配给（顺序）进程，并且通过观察可以将诸如发起者、响应者和TTP等主体指定为顺序进程来证明这一点，可能共享一些长期密钥。 为了允许在顺序进程之间共享长期密钥，我们提供了带有let绑定的E-spi演算，如let k = key（I1，I2）。P声明（和绑定）作用域P中I1和I2之间共享的长期密钥k。流程表的阅读如下。进程0是一个空进程，和往常一样什么也不做。处理new（n）。S在S本地生成一个新名称n。输入、输出、new和解密的构造基本上与Lysa演算中的相同。特别是，在Lysa中，我们预先假设了一个唯一的（匿名）公共通道，从/到该通道读取/发送消息，这种技术可以很好地模拟入侵者完全控制网络的最坏情况。与Lysa类似，我们的输入和解密构造可以通过模式匹配来测试读取（解密） 具体地，（D1，.， D m）。S读取由m个部分组成的消息，该m个部分匹配相应的Di，并继续作为S，其中由模式匹配实例化的所有变量都被其实际值替换。处理输出（D1，...，Dm）。S输出由m个部分组成的消息，然后继续作为S。模式匹配机制被定义为确保未标记的模式只匹配未标记的消息，而标记的模式只匹配标记的消息（假设标记也匹配）。因此，模式x匹配消息n（并将x绑定到n），但不匹配n：Claim（因为x未标记，而n：C已标记）。类似地，x：Claim匹配n：Claim，但不匹配n：Verif。模式匹配也适用于解密。 将x解密为{D1，. . 、Dm}d。只有当x包含一个用密钥d加密的消息，的m个部分，其匹配相应的Di。对于输入，由模式匹配实例化的所有变量在延续S中被替换。与spi演算和Lysa不同，在spi-spi演算中，我们引入了一个显式的加密结构：进程加密{D1，...，Dm}d作为x。S将变量x绑定到加密消息{D1，...，Dm}d在连续S中。这对我们的分析很有用，因为它简化了基于加密的结构检查的推理。协议的消息。最后，流程表单运行（I1，I2）。S和commit（I1，I2）声明顺序进程I1正在启动或提交与I2的协议会话。这些构造用于检查[16]中所做的对应断言示例1：我们用下面的简单（有缺陷的）身份验证协议来说明E-spi演算：1)B→A：nB2)A→B：{nB，m}kABR. Focardi，M. Maffei / Electronic Notes in Theoretical Computer Science 99（2004）267-271我们假设kAB仅由A和B知道，nB是B生成的新随机数。该协议的目的是向B保证最后一条消息是由A（最近）生成的，因为只有A应该能够加密新生成的随机数nB。 该协议可以在我们的演算中简单地形式化为如表2所示。进程启动器，生成新消息m∈N。后接收到x后，它用信号通知B开始新的认证运行，用长期密钥kAB加密x和m，然后发送加密消息。类似地，Responder生成一个新的noncenB并将其发送出去。然后，它从网络中读取y，并使用长期密钥kAB解密，检查随机数nB（通过解密的模式匹配机制）。如果匹配成功，变量z被绑定到一条消息（来自A），主体通过commit（B，A）提交。请注意，我们只对一个协议会话进行建模。然而，正如我们将看到的，通过复制Initiator和Responder进程，可以很容易地实现多个会话。表2.一个协议叙述的例子协议let k AB= key（A，B）（A，d Initiator（A，B））|B d响应者（B，A））发起者（A，B）new（m）。在（x）中。运行（A，B）。将{x，m}kAB加密为y。out（y）Responder（B，A）new（n B）. out（nB）. 在（y）中。将y解密为{n B，z}kAB。commit（B，A）操作语义学在[7]之后，用迹的形式给出了B-spi演算的操作语义消息的类别M由以下产生式定义：M：：=x|n| {M1，...，嗯嗯|M：C，包括变量，名称，和密文可能有标记轨迹可以是空的，记为“空”，也可以是s：：n其中是跟踪和操作。每一个前缀形式都产生一个相应的动作.所有可能的动作的集合，记为Act，包括由密钥分配生成的动作密钥（k，I1，I2），I d in（M1，.，M m）由输入产生，Idout（M1，.，Mm）通过输出，Idnew（n）通过限制，Id{M1，...，Mm}M通过加密和Id{M1，...，Mm}M通过解密，run（A，B）和commit（A，B）通过在CSPI演算中，通信总是在环境中执行（进程从不直接同步）。入侵者在环境中隐式建模，通过使用规则对其进行编码，这些规则形式化了操纵拦截消息的可能方式。我们用T（P）表示P的迹的集合。转换语义在[10]中正式定义。示例2：再次考虑前一示例的过程协议。以下是该过程的可能痕迹：key（kAB，A，B）：：Adnew（m）：：Bdnew（nB）：：Bdout（nB）：：Adin（nB）：：run（A，B）：：Ad272R. Focardi，M. Maffei / Electronic Notes in Theoretical Computer Science 99（2004）267-encrypt{nB，m}kAB：：Adout（{nB，m}kAB）：：Bdin（{nB，m}kAB）：：Bddecrypt{nB，m}kAB：：commit（B，A）请注意，此跟踪仅表示Ini- tiator和Responder操作的可能交错之一。在这个特定的跟踪中，commit（B，A）的前面是run（A，B）。根据Woo和Lam的通信断言思想[30]，这个跟踪是安全的，因为B确信与A通信（actioncommit（B，A）），A确实在与B运行协议（action run（A，B））。当考虑多个会话（A和B同时作为发起者和响应者运行）时，该协议是不正确的，因为它遭受反射攻击。如上所述，可以通过复制进程Initiator和Responder来对多个会话进行建模。例如，要对多个协议会话进行建模，我们可以考虑以下过程：协议2令k AB=key（A，B）。（Ad！引发剂（A、B）|Ad！应答者（A、B））|Bd！应答者（B，A）|Bd！引发剂（B，A））注意，A和B同时作为Initiator和Responder运行。实际上，新的过程发起者（B，A）和响应者（A，B）模型B分别作为发起者运行和A作为响应者运行考虑方案2的以下跟踪：key（kAB，A，B）：：Bdnew（m）：：Bdnew（nB）：：Bdout（nB）：：Bdin（nB）：：run（B，A）：：Bdencrypt{nB，m}kAB：：Bdout（{nB，m}kAB）：：Bdin（{nB，m}kAB）：：B解密{nB，m}kAB：：commit（B，A）它与上面的相同，只是B作为启动器而不是A（如粗体所示）。事实上，B正在与他自己一起运行协议，而A什么也不做。请注意，攻击是通过缺少对应关系来揭示的：commit（B，A）与任何run（A，B）都不匹配该跟踪对应于以下（众所周知的）反射攻击：1.a)B→E（A） ：nB1.b)E（A）→B ：nB2.a)B→E（A）：{m，nB}kAB2.b)E（A）→B：{m，nB}kAB我们通过基于相应断言的形式化安全定义来结束本节。在[16]中，我们说跟踪是安全的，如果每个提交（B，A）都有一个不同的运行（A，B）。如果协议的所有跟踪都是安全的，则协议保证实体认证定义2.1[安全性]一个跟踪s是安全的当且仅当每当s=s1：：commit（B，A）：：s2，则s1=sJ：：run（A，B）：：sJJ，并且sJ：：sJJ：：s2是安全的。一个进程P是安全的，如果1s∈T（P），s是安全的.1 1 1请注意，与示例2中讨论的攻击相对应的跟踪是不安全的，因为commit（B，A）与run（A，B）不匹配。R. Focardi，M. Maffei / Electronic Notes in Theoretical Computer Science 99（2004）267-2733一种组合证明技术我们的分析利用了一种标记机制的消息，使解释的某些，关键的消息组件明确。消息的未标记部分形成消息随机数标签更精细，因为它们传达了关于随机数在认证协议中所扮演角色的信息：具体地说，随机数可以在认证请求者的消息中标记为Claim，在指定预期验证者的消息中标记为Verif，或者在认证会话密钥的消息中标记为Owner证明技术适用于可以表示为形式的E-SPI过程keys（k1，.，kn）。（我1d！S1|......这是什么？| Im d! Sm）其中密钥（k1，...，k n）表示长期密钥k1，.，k;分析通过检查每个过程键（k1，.，k n）。I idSi，并且尝试在由前缀密钥（k1，.，k n）。给定进程密钥（k1，...，k n）。因此，我们对长期密钥和会话密钥在主体和可信第三方之间流通的方式做出以下假设，即：（a）长期密钥从不以明文或在加密分组内流通;（b）只有主体可以接收会话密钥，而不泄露它们;以及（c）新的会话密钥仅由TTP分发给 当满足这些假设时，我们说密钥（k1，...，k n）。IdS是{k1，...，kn}-安全。这在[10]中得到了充分的证实。证明规则（表3和表4）相对于给定的身份和两个环境来验证协议的每个主体和可信方，即，它们对于与恒等式有关的顺序过程S得出形式I;我和两个环境分别是。 历史环境的变迁每个加密、解密、运行和密钥分配发生在由所讨论的一方执行的动作随机数环境保存该方生成的随机数5。当一个nonce由一个新的前缀引入时，它首先被包含在随后，可以通过模式匹配来检查随机数，并且在规则（A_AUTHENTICATE_CLAIM）、（A_AUTHENTICATE_OWNER）和（A_AUTHENTICATE_VERIF）（在表3中）中如此标记随机数。证明规则被定义为确保每个随机数最多可以被检查一次。我们将在案例研究中应用规则时解释规则背后的直觉[5]我们写（x）=enc{. . }d表示x<$→enc{.. . }d∈，对于其他条目也是如此。我们写（·）=enc{. . }d来表示存在x，使得{x}=enc{.. . }d.274R. Focardi，M. Maffei / Electronic Notes in Theoretical Computer Science 99（2004）267-局部正确性，对于一个顺序的过程，可以建立提供的过程符合上述的关键安全假设定义3.1 [局部正确性]设P为进程密钥（k1，.，kn）。IDS，与ki在Ii和Ji之间共享。P是局部正确的，如果判断I; kk1，...，knS是表3局部正确性：主体和TTP规则申请人和验证人规则一个真实的CCLAIMA; Id，n：已检查; =dec{B：Id，n：Claim. }k∈{key（A，T），key（A，B）}A; n，n：unchecked;未检查commit（A，B）。S一个真正的赢家A; ID，n：已检查; =dec{B：Id，n：Owner，y：Key. }kAT{kAT}=key（A，T））=dec{D1，. ..，DJ}yJ暗示了S.t. DJ不匹配Di）1百万iA; n，n：unchecked;未检查commit（A，B）。S一个真实的VERIFA; n：已检查; =dec{A：Id，n：Verif. }kAB<$（kAB）=key（A，B）A; n，n：unchecked;未检查commit（A，B）。SC·莱芒A;;。y<$→ enc{A：Id，x：Claim}k S（kAB）= key（A，B） =J. B›→运行A;;encrypt{A：Id，x：Claim. }kAB为y。S奥沃纳A;;。y→ enc{D1，. ，Dm}x S验证器（·）=dec{B：Id，n：Owner，x：Key. }kAT（kAT）=key（A，T） =J. B›→运行A; n;n加密{D1，. ，Dm}x作为y。SRUNA;;。y<$→ enc{B：Id，x：Verif}k <$S <$（k）∈ {key（A，T），key（A，B）}<$=<J. B›→运行A;验证;加密{B：Id，x：Verif. }k为y。SA;;。B<$→run_S_A;_;_run（A，B）. STTP规则TTP FORWARD CHECKT;，n：检查;。y›→ enc{A：Id，x：Claim}kBT 公司简介（·）=dec{B：Id，n：Verif. }kAT=key（A，T）T; n，n：unchecked;未检查加密{A：Id，x：Claim. }kBT作为y。STTP向前T;;。y›→enc{A：Id，x：Claim}kBTS（·）=dec{B：Id，x：Verif. }kAT=key（A，T）T;encrypt {A：Id，x：Claim. }kBT作为y。STTP DIAPARTET;;。y›→ enc{A：Id，x：Owner，ks：Key}kBT 公司简介加密{A：Id，x：Owner，ks：Key. }kBT作为y。SR. Focardi，M. Maffei / Electronic Notes in Theoretical Computer Science 99（2004）267-275表4局部正确性：通用主规则通用主要规则NILI;;0极输入I;;NEWI;，n：未检查;n新鲜I; n;.新的。S输出I;;加密I;in（.）. S我;我;我出去了。SI;;。y> → enc{d1，. ，dm}d S（·）=dec{.，d：Key，. }k 表示n= nJ。B›→运行。x›→enc{. }d.I; i;i加密{d1，. ，dm}d作为y。S解密I;;。y> → dec{D1，. ，Dm}d SI; i ; i;i解密y为{D1，. ，Dm}d. S可导出，对于k1，.，kn = k1 <$→ key（I1，J1），.，kn → key（In，Jn），并且S是{k1，.，kn}-安全。最后，一个过程是正确的，如果它的所有顺序组件都是局部正确的。定义3.2 [过程正确性]设P=keys（k1，.，kn）。（我1d！S1|···|我md！Sm）。 P是正确的，如果进程密钥（k1，.，kn）。我我 dSi是局部正确的，对于所有i∈ {1，.， m}我们的主要结果表明，在定义3.2的意义上，正确性是安全性的充分条件（定义2.1），因此，是保证实体认证的充分条件形式上：定理3.3（全局安全性）设P=keys（k1，...，kn）。（我1d！S1|···|我是D！Sm）。如果P是正确的，那么它是安全的[10]。4案例研究在本节中，我们将分析一些著名的身份验证协议。给出我们可以证明它的安全性，或者在协议有缺陷的情况下，我们展示如何修复它以证明正确。在4.1中，我们分析了ISO对称密钥双向单边认证协议[21]，在4.2中分析了基于nonce的宽口青蛙协议[4]，在4.3中分析了Woo和Lam认证协议[29]，在4.4中分析了修正的Needham Schroeder共享密钥协议[28]。？？卡尔森密钥发起协议（Carlsen 's Secret Key Initiator Protocol）[ 11]276R. Focardi，M. Maffei / Electronic Notes in Theoretical Computer Science 99（2004）267-4.1ISO对称密钥双向单向认证协议在本节中，我们将我们的分析应用于ISO对称密钥两遍单向认证协议[21]。这种直接认证协议的目的是对A和B进行认证。(1)B→A：nB(2)A→B：{B，nB，m}kAB在第一个消息中，B向A发送一个挑战。A接收随机数并将其与B的身份标签一起加密。B接收密文，通过检查之前发送的随机数和密文中的随机数之间的相等性来检查消息的新鲜度，并且在操作成功的情况下，接受来自A的认证请求。密文中的身份标签B避免了反射攻击（参见第2节）。通过我们的技术分析该协议的第一步是适当地标记它：nB用于检查消息的新鲜度，其中身份标签B指定预期的验证者。因此，B被Verif标记为Id和nB。请注意，标记使消息组件的角色更加清晰。(1)B→A：nB(2)A→B：{B：Id，nB：Verif，m}kAB方案代码见表5。每个结构右侧的规则名称总结了分析的步骤。表5ISO对称密钥双向单向认证协议协议isolet k AB=key（A，B）。（A d）引发剂iso（k AB，A，B）|B d应答者iso（k AB，B，A））引发剂iso（kAB， A， B）new（m）.N EW在（x）中。极输入运行（A，B）。R UN将{B：Id，x：Verif，m}kAB加密为y。 验证器输出（y）OUTPUT应答者iso（kAB，B，A）new（nB）.N EWout（nB）.输出在（y）中。极输入将y解密为{B：Id，nB：Verif，z}kAB。 D.开裂commit（B，A）验证设kAB = key（A，B）的局部正确性。Ad引发剂iso（kAB，A，B）可如表6中证明。规则（NEW），（IINPUT），（RUN）和（OUTPUT）的假设被简单地验证;唯一有趣的情况是（VERIFIER），它被应用于证明A;{m：unchecked}; kAB ›→ key（A，B）. B›→运行加密{B：Id，x：Verif，m}kAB作为y。out（y）规则（CLAIMANT）、（VERIFIER）和（OWNER）形式化了A可以声明她向B认证的意愿的方式。这就是为什么他们要求运行（A，B）R. Focardi，M. Maffei / Electronic Notes in Theoretical Computer Science 99（2004）267-277表6引发剂iso（kAB，A，B）：安全性证明A; n;kAB <$→ key（A，B）n new（m）. 在（x）中。运行（A，B）。将{B：Id，x：Verif，m}kAB加 密为y。out（y）↓（东北）A;{m：unchecked}; kAB <$→ key（A，B）在（x）中的值。运行（A，B）。将{B：Id，x：Verif，m}kAB加密为y。out（y）（INPUT）A;{m：unchecked}; kAB›→ key（A，B）删除run（A，B）。将{B：Id，x：Verif，m}kAB加密为y。out（y）↓（RUN）A;{m：unchecked}; kAB›→key（A，B）. B›→运行加密{B：Id，x：Verif，m}kAB作为y。out（y）↓（验证器）A;{m：unchecked}; kAB›→key（A，B）. B›→运行。y›→enc{B：Id，x：Verif，m}kAB输出（y）↓（OUTPUT）A;{m：unchecked}; kAB›→key（A，B）. B›→运行。y›→enc{B：Id，x：Verif，m}kAB0（尼加拉瓜）表7应答者iso（kAB，B，A）：安全性证明B; n;kAB <$→ key（A，B）n new（nB）. 在（y）中。将y解密为{B：Id，nB：Verif，z}kAB。commit（B，A）↓（东北）B;{nB：unchecked}; kAB <$→ key（A，B）在（y）中的值。将y解密为{B：Id，nB：Verif，z}kAB。commit（B，A）（INPUT）B;{nB：unchecked}; kAB ›→ key（A，B）将y解密为{B：Id，nB：Verif，z}kAB。commit（B，A）↓（D收缩）B;{nB：unchecked}; kAB ›→ key（A，B）.y<$→dec{B：Id，nB：Verif，z}kAB提交（B，A）↓（A真实验证）B;{nB：checked}; kAB ›→ key（A，B）.y›→dec{B：Id，nB：Verif，z}kAB0（尼加拉瓜）已经被处决了具体地，在（验证器）中，A可以通过发送消息{B：Id，x：Verif. . }kAB到B使用与B共享的长期密钥kAB。正如预期的那样，角色Verif用于通知B他是当前身份验证会话的预期验证者。规则（验证者）也可以被A用来通知TTP TB是预期的验证者。在这种情况下密文使用A和T之间共享的长期密钥进行加密（参见4.2和4.3节）。（ VERIFIER ） 要 求 B<$→run 是 历 史 环 境 中 的 最 后 一 个 元 素 ， 并 且kAB<$→key（A，B）属于历史环境，这两个条件都为真。设kAB = key（A，B）。响应者iso（kAB，B，A）相关，本地正确-如表7所示。278R. Focardi，M. Maffei / Electronic Notes in Theoretical Computer Science 99（2004）267-i，j=1，ij<证明了letkAB=key（A，B）的局部正确性。BdResponderiso（kAB，B，A）是简单的。唯一有趣的情况是（AUTHENTICATE VERIF），它被应用于证明B;{nB：unchecked}; kAB ›→ key（A，B）. y<$→dec{B：Id，nB：Verif，z}kAB提交（B，A）规 则 （ AAUTHENTICATECLAIM ） 、 （ AAUTHENTICATEOWNER ） 和（AAUTHENTICATE VERIF）形式化了主体A验证另一主体的三种可能方式B. 具体地说，（AAUTHENTICATE VERIF）指出，只有当A先前生成了一个随机数n并解密了一条消息时，A才可以合法地提交（因此认证）B{A：Id，n：Verif.. . }kAB（具有相同的随机数），其中k与B共享。（A验证）假设成立，因为y<$→dec{B：Id，nB：Verif，z}kAB属于历史环境，而nb：unchecked属于现时环境。请注意，此规则检查随机数：这就是为什么nB的绑定移动到checked。此外，如（AUTENTICATE VERIF）所要求的，历史环境还包含kAB<$→key（A，B）。因为（NEW）、（O输出）、（I输入）和（解密）是平凡满足的，B;kAB<$→key（A，B）<$Responderiso（kAB，B，A）。最后，该协议不使用会话密钥，并且长期密钥既不在网上发送也不加密。因此，发起者和响应者代码都是密钥安全的，因此可以被判断为正确的。通过定理3.3，我们直接得到了ISO协议的每一个踪迹都是安全的，因此不可能进行认证攻击这个例子阐明了我们的证明系统是如何分析直接认证协议的：其思想是，只有在特定形式的密文先前已被解密的情况下，提交（B，A）才能被证明该密文必须遵循其中一个原则进行加密，在本例中（验证器）。这保证了run（A，B）先前已经被断言。由于随机数只能被检查一次，在协议生成的每个跟踪中，每个提交（B，A）之前都有一个不同的运行（A，B）。请注意，Protocoliso仅对一个协议会话进行建模，因此可以认为攻击可能发生在多个会话上。然而，这是不正确的，因为我们的技术是完全组合的，并保证即使顺序进程Initiatoriso和Responderiso被任意复制，Protocoliso也是安全该规范可以推广到任意数量m的实体，作为发起者和响应者，任意复制。协议iso−mletmk ij= key（I i，I j）.Mi，j=1，i/=j我知道！初始化器iso（k ij，I i，I j）|我知道！响应者iso（kij，Ii，Ij）kij表示在实体Ii和Ij之间共享的长期密钥。 我们假设kij=kji（并且相应地仅为键kij定义键分配，ij）。<使用适当的长期密钥，针对每对实体Ii、Ij任意复制发起者iso和响应者iso。的正确性证明（|R. Focardi，M. Maffei / Electronic Notes in Theoretical Computer Science 99（2004）267-279i，j=1，ij

下载后可阅读完整内容，剩余1页未读，立即下载