理论计算机科学电子札记173（2007）85-102www.elsevier.com/locate/entcs子、同态和子：描述协议执行1沙丁湾Doghmi多格米2，5美国加利福尼亚州斯坦福大学约书亚·D 古特曼3The MITRE CorporationBedford，MA，美国F.哈维尔·塞耶4The MITRE CorporationBedford，MA，美国摘要在本文中，我们开发了一个框架，串空间的基础上，推理密码协议和其执行的特点。我们定义骨架、同态和形状。密码子对有关密码协议执行中的规则（诚实）行为的部分信息进行建模。骨架之间的同态是信息保持映射。许多协议分析可以看作是对骨架和同态范畴性质的探索。一组骨架可以表征协议的所有运行;最小的这样的集合是形状的集合。这种方法是协议分析机械化的基础。关键词：协定分析，串空间，列举协定执行，机械化协定分析。1介绍大多数协议分析工具和技术都基于公式，证明或反驳以特定逻辑表达协议安全目标的开始1由国家安全局和MITRE赞助的研究提供支持。2电子邮件地址：shaddin@cs.stanford.edu3电子邮件地址：guttman@mitre.org4电子邮件地址：jt@mitre.org5这项研究是作者在MITRE公司工作时进行的。1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.02.02986S.F. Doghmi等人/理论计算机科学电子笔记173（2007）85从一些初始假设，定理证明或模型检查（如[9]）技术可以用来检查是否从协议定义遵循某种安全属性在本文中，我们采取不同的方法来解决这个问题。而不是单独检查每个安全属性，我们的特点是所有的协议执行兼容的初始假设。所得到的特征是一组代表所有可能的方案运行的方案运行。这些代表是协议的最小的、本质上不同的执行。这种方法的一些优点是：. 我们发现，不同的安全属性的证明往往重复相同的工作。使用这种方法，表征可能运行所需的所有工作可以一次完成。然后，分析人员或简单的工具很容易. 设计者没有预料到的协议的安全属性将变得明显。. 对某个安全属性感兴趣的分析师可以看到所有可能的攻击/反例，而不是单个攻击。. 由于所有可能的协议运行表示，这使协议设计者更深入地了解用于构建协议的不同原语的效果。在本文中，我们将提出一个框架，串空间的基础上，分析协议和表征其执行。虽然我们的特征的广义概念可以捕获认证和保密属性，我们在这里专注于一个更简单的概念，专门捕获认证属性。我们将在其他地方讨论保密的适用性。在实践中，任何构造特征的算法都必须考虑保密性和认证性。作为这个框架的动机，考虑一个协议分析师提出了一些关于协议运行的初始假设。通常这是一个单一的参与者的经验和一些秘密和新鲜的假设。然后，分析人员可以重复应用推理规则，例如身份验证测试[4]，来推断更多关于协议运行的结构。在分析中的任何一点，分析员都拥有关于可能的方案运行结构的部分信息。我们将用我们称为骨架的结构来表示这部分信息。我们还将定义骨架之间的同态概念;同态是信息保持映射。因此，许多协议分析可以用骨架和它们之间的同态来表示。我们在[2]中讨论了用于构造这些特征的实际算法。在本文中，我们定义了算法的基本框架。给定一组初始假设（初始框架），我们将定义一组协议运行如何表征所有可能的运行。此外，我们将表明，有一个最小的这样的特征：形状的集合。它们是本议定书可能的S.F. Doghmi等人/理论计算机科学电子笔记173（2007）8587¨BB一K一K¨¨B一BKBB初始化响应• Na，A）¨Na，A）·¨{|Nb，Na，A|}K−1{|Nb，Na，A|}K−1（¨（？¨{|N J，N，B|}−1一{|N J，N，B|} −1一·））·Fig. 1. ISO候选协议初始化响应·Na，A）·¨ ¨{ 1}|Nb，Na，A|}K−1（）¨ ¨{|N J，N，B|} −1一·）·图二. 捆绑包：预期运行2一个激励的例子图1所示的协议是ISO委员会考虑的纯认证协议[3]的候选者没有实现共享秘密它对数字签名使用图1给出了协议的角色。两个垂直列中的每一个描述参与协议的主体可以遵循的行为。左边的列发起会话，而右边的列是响应者的行为。任何主要的爱丽丝，鲍勃，等等，可以参与这些角色中的任何一个，或者可能同时参与每个角色的几个协议的实际运行由这些角色的任何有限数量的实例组成，通过消息传输和（可能的）对手的动作连接。我们将由双箭头连接的垂直列称为串，并使用它来表示执行协议的主体的单个本地会话，或者是对手活动的序列。有一种执行只是连接相应的箭头，它模拟一个会话，在该会话中，主体（这里称为A和B）发送的消息到达它们的目的地（图2）。我们把这种执行称为捆绑。这是一小捆。有无限多个更大的束由这个图的多个副本组成，可能具有不同的参数值。然而，较大的执行与图2的执行没有本质的不同。然而，该议定书被委员会拒绝，因为他们发现，¨88S.F. Doghmi等人/理论计算机科学电子笔记173（2007）85¨B一¨¨·一Np，ArespP）B¨ ¨{|Nb，NP，A|}K−1resp（¨·（·¨Nb，B？¨¨{|Na，Nb，B|}K−1<$·）？¨¨{|Na，Nb，B|}K−1·）·图三. 英文名：The Canadian Attack另一种本质上不同的执行是可能的[3]，如图3所示。由于它是由加拿大在委员会的代表发现的，因此有时被称为加拿大攻击[3]。攻击者用P表示。攻击涉及两次响应者角色，都是由对手发送的消息刺激的从响应者B的角度来看，该攻击构成认证失败。即使B和A都有未泄露的私钥，协议也不能向响应者B保证A正在运行发起者角色的相应实例。在这次攻击中，A正在运行响应者角色的实例，尽管只执行了该角色的前两步;A正在等待第三此会话的消息，尽管它永远不会被传递。假设这些都是最小的，本质上不同的执行可能包含一个响应者运行使用未泄露的私钥。在这种情况下，我们可以读取o，B获得的认证程度。B在响应者会话结束时知道已经存在与B的会话在参与者的身份和参数N a、N b上一致的A但是，B无法知道它是长度为3的发起者角色还是长度为2的响应者角色，因为每个角色都存在执行。由于协议设计者希望确保B知道有一个匹配的启动器运行，因此该协议太弱，无法满足目标。3形的观念在接下来的讨论中，我们将使用术语规则链来指代协议的某个角色的运行。同样，我们将使用常规节点来表示发生在常规链上的发送或接收事件我们还使用常规行为来指代协议特定运行中的所有常规节点以及它们的因果排序。我们还将使用符号项（n）来表示在节点n上发送或接收的消息。在实践中，协议的形式非常少。上面介绍的ISO拒绝协议有两个，如果我们从响应者的角度来看，询问全局¨¨¨¨¨S.F. Doghmi等人/理论计算机科学电子笔记173（2007）8589¨B一KBB一K一K一¨一K一K一一BBBBBNa，A ）B¨{|Nb，Na，A|}K−1（？¨{|N J，N，B|} −1一）·non={K−1，K−1}A Bunique={Nb}见图4。 ISO候选应答器框架Na，A≤Na，A（A）。...........................................）B？¨ ¨{|Nb，Na，A|}K−1≥{|Nb，Na，A|}K−1（............................................ （？¨ ¨{|N J，N，B|}−1一联系我们|N J，N b，B|} −1一•）......non={K−1，K−1}）·A Bunique={Na，Nb，NJ}图五. ISO候选预期形状Na，A ）B¨N、B联系我们|Nb，Na，A|}K−1（¨..................................... （ ？¨{|N J，N，B|}−1一联系我们|N J，N b，B|} −1一•）.......non={K−1，K−1}）·A Bunique={Nb，NJ}见图6。 ISO候选攻击形状如果B在本地运行协议，则必须发生行为在ISO拒绝协议中，我们假设B假设响应者B完成了协议的运行执行4中所示的股。 一定是发生在其他地方网络？有两种可能。90S.F. Doghmi等人/理论计算机科学电子笔记173（2007）85一一一一3.0.1ISO认证响应者收到的最后一条消息已经由未泄露的私钥K-1签名。让我们考虑消息起源于发起者链的情况。 在这种情况下，启动器A必须具有部分匹配strand，消息以预期的顺序发送和接收。这在图中描绘五、消息发送和接收的顺序可以通过对随机数Nb的新鲜度假设以及任何规则串生成新鲜随机数（在这种情况下为Na和NJ）的假设来推导。 该顺序由以下箭头表示：这两种类型和连接符号≤。 这些符号意味着是有序的，但其他行为可能会介入，无论是敌对的链还是常规的链。另一种可能性是签名的消息起源于响应者链。在这种情况下，我们可以使用类似的分析来推断图6中的事件一定是按该顺序发生的。除了这两种形状之外，没有其他选择。任何包含图4所示的应答链的图必须包含一个起始链，其事件顺序如图4所示5，或响应链与事件排序如图。六、这样的图形是一种形状。形状由一些执行的规则股组成，形成包含初始规则股的最小集合（在本例中，仅为右侧列）。可能的处决可能会自由地增加对手的行为。每个形状都与关于密钥和新鲜度的假设有关，在这种情况下，K−1是不妥协的，Nb是新选择的，而且规则链生成新的随机数。在寻找形状的过程中，人们从一些初始的线开始。通常，初始集是一个单例，我们称之为分析的同态，同态，同态。新引入的术语在本节中以黑体骨架A是（1）一组有限的规则节点，配备了额外的信息。附加信息包括：（2）节点上的偏序≤A，表示因果优先;（3）一组键非A;（4）一组原子值唯一A。非A中的值必须不起源于A，而唯一的A在A中至多起源一次。6（见定义）5.1.）我们说骨架A是实现的，如果它恰好具有某些执行的常规行为。常规串接收到的每个消息要么应该是以前发送过的，要么应该是对手可以使用以前发送的消息构造的。例3.1图5显示骨架Aiso1，非A={K-1，K-1}，唯一的A ISO1={Na，Nb，NJ}。iso1是一个已实现的骨架。异源蛋白A B图6示出了骨架Aiso2。该框架是实现的，并描述了对协议的攻击中有规律的错误.6当n∈ A且n ≤ Anj时，我们要求n∈ A且n≤AnJ。S.F. Doghmi等人/理论计算机科学电子笔记173（2007）8591→→图4中描绘的单个响应链也形成骨架Ab，非，如图所示的唯一AB没有实现。Ab的前两个节点也形成骨架Ab2。这个骨架是实现的，因为对手可以准备其第一个节点的传入消息，并丢弃其第二个节点的传出消息同态是从A0到A1的映射H，记为H：A0→A1。 我们将其表示为一对映射（φ，α），其中φ将A0的节点映射到A1的节点，α是将原子值映射到原子值的替换 我们写t·α表示将替换α应用于消息t的结果。H=（φ，α）是一个同态：（1）φ表示串结构，且对所有n∈A0，term（n）·α= term（φ（n））;（2）m≤A0n蕴涵φ（m）≤A1φ（n）;（3）nonA0·α≠nonA1;（4）uniqueA0·αuniqueA1.（定义。（第4.1、5.6段）同态是信息保持变换。每个骨架A0描述了从A0通过同态可达的已实现骨架。由于同胚合成，如果H：A0→A1，则任何从A1可达的已实现骨架都可以从A0可达。因此，A1保留了A0中的信息：A1描述了由A0描述的已实现骨架的子集。同态可以用A1中的额外行为来补充A0的链;它可以选择原子参数值;如果不同的节点在发送的消息和部分排序中的位置是兼容的，例3.2将图4中的骨架嵌入图5中的骨架的映射H：AB→Aiso1是同态。同样，如果我们将B考虑骨架Aiso1的变体AJ，我们将变量A重命名为B（即，我们识别A和B）。 有一个同态HJ将Ab映射到AJ，像H一样嵌入，但也将A重命名为B。同态H=（φ，α）是逐点内射的，如果函数φ在节点上是内射的.节点单射同态决定了同态的一个有用的偏序：当对某个节点单射H1，H1<$H=HJ，我们写H≤nHJ.若H≤NHJ≤nH，则H和HJ同构。我们说同态H刻画了所有已实现的同态HJ使得H≤nHJ。同态H：A0→A1是一个形状i ∈（a）A1是实现的，（b）H是从A0到实现骨架的同态中的≤n-极小如果H是一个形状，我们可以把H分解成A0H0 AJH1A1，其中AJ被实现，则AJ不能包含比A1更少的节点，或者标识更少的原子值。1是尽可能小和一般。（Def. 7.8.）当同态H（通常是嵌入）被理解时，我们称骨架A1在这个更宽松的意义上，图5和图6都描绘了形状。严格地说，嵌入Hiso1：Ab→Aiso1和Hiso2：Ab→Aiso2是形状。如果H：A0→A1且A1已实现，则形状集H1且H1≤nH是有限且非空的。92S.F. Doghmi等人/理论计算机科学电子笔记173（2007）854背景在本节中，我们定义核心链空间概念。我们定义项的代数A。A中的术语是通过构造函数从原子术语构建的。原子术语被划分为主体、文本、键和随机数类型。逆运算符是在键上定义原子上可能有其他操作，例如函数的单射公钥或单射长公钥。将主体映射到键的函数的术语共享键原子作为变量（indetermi- nates），用斜体字表示（例如a、Na、K−1）。我们假设A包含每种类型的无限多个原子A中的项是使用连接和加密从原子自由构建的。t0和t1的连接记为t0，t1.加密采用项t和原子密钥K，并产生写为{|不|K.为了简单起见，我们使用替换而不是一般的替换。置换只有原子在其范围内：定义4.1[置换，应用]置换是一个函数α，它将A中的原子映射到A中的原子，使得（1）对于每个原子a，α（a）是与a相同类型的原子，（2）α是关于原子上的操作的同态，例如：在逆密钥的情况下，对于每个密钥K，K−1·α=（K·α）−1。α对t的应用，记作t·α，同态地扩展了α更明确地，如果t=a是原子，则a·α=α（a）;并且：（t0，t1）·α =（t0·α），（t1·α）（{|不|}K）·α={|t·α|}K·α应用程序通过配对和集合进行分发因此，（x，y）·α=（x·α，y·α），且S·α={x·α：x∈S}。如果x/∈A是一个简单的值，如整数或符号，则x·α=x。对于本文和即将进行的工作来说，将我们自己限制在替换位置是一种方便的简化。然而，我们的模型是可扩展的，可以使用更一般的替代概念我们可以在今后的工作中关注这一点由于置换将原子映射到原子，而不是复合项，因此统一非常简单。如果t1·α=t2·α，则替换α统一t1和t2。两个项是可统一的，当且仅当它们具有相同的抽象语法树结构，在对应的叶子上具有相同的原子类型。如果t1，t2是可统一的，那么t1·α和t2·β也是可统一的。任何两个可单位项t1，t2都有唯一的（直到重命名）最一般单位元。方向+表示发送，方向−表示接收：定义4.2 [Strand Spaces]方向是符号+、−之一。有向项是一个对（d，t），其中t∈A，d是一个方向，通常写作+t，−t。（±A）是有向项的有限序列的集合。A上的串空间是一个结构，它包含一个集合A和两个映射：一个迹映射tr：A→（±A）A和一个替换应用算子（s，α）→s·α，使得（1）tr（s·α）=（tr（s））·α，（2）s·α=SJ·α蕴涵s=SJ。要素S.F. Doghmi等人/理论计算机科学电子笔记173（2007）8593B线被称为线。根据条件（2），任何非平凡的S都有无限多个每个链S的副本，即，具有tr（SJ）=tr（s）的股SJ请注意，在本文中，当我们提到一个串时，我们也隐含地提到了它的迹。定义4.3侵彻体股线具有下列形式之一的痕迹：M：+t其中t ∈文本，主，随机数K：+KC：−g，−h，+g，hS：−g，h，+g，+hE：−K，−h，+{|H|}KD：−K−1，- {|H|}K，+h，如果s是一个侵彻体股，则s·α是一个同类的侵彻体股定义4.4[协议]一个协议n =rR，n，ur由以下部分组成：（1）一个有限的链集合R，称为协议的角色;（2）对于每个角色r∈R，两个原子集合nr，ur给出r的起源数据。环R上的正则链R_n由所有迹为r·α的链组成，其中r∈R和α是置换的。例4.5图1描述了ISO的RTP协议。请注意，发起者角色的数据指示任何诚实的发起者具有未泄露的私钥K-1，并且他生成新的随机数Na和NJ。同样，任何一诚实的响应者有一个未泄露的私钥K-1一并产生新鲜nonceNb.节点是一对n=（s，i），其中i≤length（tr（s））;strand（s，i）=s;n的方向和项是tr（s）（i）的方向和项。 我们称一个节点n=（s，i）是正则的，如果s是规则链，并且相关的协议被理解。 我们更喜欢写对于节点n=（s，i），s↓i。 所有节点的集合N形成一个有向图G=<$N，（→ <$N）<$N，其中边n1→n2用于通信（具有相同的项，从正节点指向负节点），n1<$n2用于在同一条链上的连续。子项关系，写作<$，是最小自反的传递关系，如that（1）t0<$t0，t1;（2）t1<$t0 ， t1; 和 d （ 3 ） t<${| 不 |K.Notice ， howeverr ， Kи/{1}| 不 |}Kunless（unless）K<$t.我们说一个原子a存在于项t中，如果aиt。我们说密钥K用于项t中的加密，如果对于某个t0，{|的t0|好的。如果a在t中出现或在t中使用，则a在t中被提及。如果n为正数，则项t起源于节点n，t<$term（n），并且t术语（m）当m≠n时，因此，如果t是在n上传输的消息的一部分，则t起源于n。n，并且t在此链上先前既没有发送也没有接收。定义4.6[丛] G的有限无圈子图B=<$NB，（→B<$$>B）<$是丛，如果（1）如果n2∈NB 是 负 的 ， 则 存 在 唯 一 的 n1∈NB 且 n1→Bn2; （ 2） 如 果 n2∈NB 且 n1<$n2 ， 则n1<$Bn2。当B是丛时，≤B是（→ B B）的自反传递闭包。一个丛B是环B上的丛B，如果对每一个s↓i∈ B，（1）s∈R，n，u ∈R;（2）如果s=r·α且a∈nr·α，则a不起源于B;（3）如果s=r·α且a∈ur·α，则a至多起源于B一次。94S.F. Doghmi等人/理论计算机科学电子笔记173（2007）85例4.7图2和图3描述了图1命题4.8设B是一个丛。≤B是一个良基偏序。B的每个非空节点集都有≤B-极小成员。如果α是置换，则B ·α是丛。我们还将定义丛之间的子丛关系定义4.9丛B1是丛B2的子丛，如果B1是B2，直到节点的（内射）重命名。5子与同态在本节中，我们将定义骨架和同态的框架preskeleton描述了一组束的规则（诚实）部分。定义5.1一个四元组A=（node，≤，non，unique）是preskeleton，如果：(i) 节点是有限个正则节点集，n1∈节点且n0∈+n1蕴涵n0∈节点;(ii) ≤是结点上的偏序，使得n0≤n1蕴涵n0≤n1;(iii)non是一组密钥，其中如果K∈non，则对于所有n∈节点，K对于某个nJ∈节点，K或K−1用于项（nJ）;项（n），以及(iv) unique是一组原子，其中如果a∈unique，对于某个n∈节点，a<$term（n）。一个preskeletonA是一个骨架，如果此外：(v) a∈unique意味着a起源于不超过一个n∈节点。一 个骨 架类 似 于[9] 中 的半 丛概 念 。我 们之 所 以同 时定 义 preskeletons 和skeletons，是因为preskeletons是骨架的前身人们可以通过统一和组合源自同一个原子a∈unique的链来将preskeleton转换为骨架。我们使用下标选择一个preskeleton的组件。例如，如果A=（node，R，S，SJ），则≤A表示R，唯一A表示SJ。 我们写n∈A表示n∈节点A，当s的至少一个节点在A中时，我们说串s在A中A. s的A-height是s在A中的节点数。根据第三条和第四条，uniqueA=唯一A我们将以类似于子丛关系的方式定义子[前]骨架关系定义5.2一个[前]骨架A是AJ的子[前]骨架，如果每个节点A，≤A，nonA，uniqueA分别是节点Aj，≤AJ，nonAJ，uniqueAJ的子集，直到节点的（injective）重命名束对应于某些骨架：定义5.3丛B实现骨架A，如果（1）A的节点恰好是B的正则节点;（2）仅当n，nJ∈节点A且n≤BnJ时，n≤Anj;（3）K∈非AS.F. Doghmi等人/理论计算机科学电子笔记173（2007）8595仅当K/иterm（n）对于任何n∈ B，但K或K−1用于某个nJ∈ B时;（4）a∈唯一A仅当a唯一起源于B时。如果某个B实现了A，我们说A是一个实现的骨架。例5.4图2中的运行包实现了图5中5. 同样，图3中的攻击包实现了图6中的框架。事实上，一个bundle完全决定了它实现的框架命题5.5如果B是一个丛，那么它实现了一个唯一的骨架。根据条件（4），如果A是preskeleton但不是skeleton，则B不实现A。同态。由于preskeleton表示协议运行的部分信息，因此定义它们之间的信息保持映射将是有用的：同态定义5.6设A0，A1是预骨架子，α是置换子，φ：节点A0 →节点A1.H=[φ，α]是同态，如果(i) 对所有n∈A0，term（φ（n））= term（n）·α;(ii) 对所有的s，i，如果s↓i∈A，则存在一个sJs. t.对所有j≤i，φ（s↓j）=（sJ，j）;(iii) n≤A0 m表示φ（n）≤A1φ（m）;(iv) nonA0·α-nonA1;(v) uniqueA0·αuniqueA1.当H是从A0到A1的同态时，我们记为H：A0→A1.同态可以通过收缩源自相同a∈唯一A的节点来将预骨架变换为骨架。此外，同态可以将preskeleton转换为实现的骨架。存在与由preskeletonA表示的一组起始序列兼容的协议的许多运行。从A到实现的骨架的同态描述了A如何成为协议运行的一部分。定义5.7如果同态H将A映射到一个已实现骨架Aj，则我们说同态H实现了预骨架A。在这种情况下，我们说A是可实现的。实现的骨架是通过恒等同态可实现的preskeleton。6简并我们使用唯一起源的概念来表示新生成的值，如随机数和会话密钥。这就需要我们把我们感兴趣的同态集限制为尊重唯一起源的这种预期的现实世界意义的同态定义6.1[退化同态]如果存在不同的原子a，b和链s，则A的替换α是退化的，其中（1）a∈唯一A起源于A中的s↓i，（2）b出现在s↓j上，j≤i，（3）a·α=b·α。96S.F. Doghmi等人/理论计算机科学电子笔记173（2007）85BB一K一K一Na，A≤Na，A（A）。....................................¨）B？¨{|Na，Na，A|}K−1≥{|Na，Na，A|}K−1（..................................... （？¨ ¨{|N J，N a，B|}−1一{|N J，N a，B|}−1一•）.......non={K−1，K−1}）·A Bunique={Na，NJ}见图7。 退化同态H=[φ，α]：A0→A是退化的，如果α对A0是退化的.简并置换将一个唯一起源的原子与在它被选择时已经知道的例如，通过标识Na和Nb将图5中的骨架映射到图7中的骨架的同态是退化的。退化同态相对于协议的随机模型具有可忽略的概率[5]。在本文的其余部分中，读者可以假设每个对同态的引用实际上都限于非退化同态。本着同样的精神，我们只对尊重独特起源的现实意义的[前]骨架/捆绑感兴趣定义6.2[退化Preskeleton/丛]一个[前]骨架/丛是退化的，如果它包含角色r的串r·α，使得（1）a∈ur起源于r↓i（2）b出现在r↓j（j≤i），并且（3）a·α=b·α。图7中的骨架是退化的。 同样，读者可以因为，每一个提到[前]骨架/束都被限制为非退化[前]骨架/束。7形状7.1李约瑟·施罗德我们看到ISO拒绝协议有两个形状，一个对应于预期运行，另一个对应于攻击。Needham-Schoeder- Lowe [7，6]方案只有一个形状，对应于预期运行。这适用于NSL，无论我们采取响应者B的观点，询问如果B已经进行了协议的本地运行，那么必须发生什么全局行为，或者我们是否从发起者A的本地运行开始。无论哪种情况，另一方都必须有一个匹配的运行。然而，A永远无法确定它发送的最后一条消息是否被B接收到，因为A不再期望接收任何进一步的消息。对于像Needham-Schroeder-Lowe这样强大的协议，形状的统一性可能并不奇怪。≤S.F. Doghmi等人/理论计算机科学电子笔记173（2007）8597一BJB初始化响应•{|N a，A|}KB）¨{1}|N a，A|}KB ）·¨{|N a• （¨，Nb|}KA{|N a（，Nb|}KA·¨{|N b|}KB{|N b|}KB·））·noninit={K−1}nonresp={K−1}A Buniqueinit={Na}uniqueresp={Nb}见图8。 李约瑟·施罗德协议{|N a，A|}KBJ联系我们|N a，A|}KB（A）。....................................¨）B？¨{|N a，Nb|}KA联系我们|N a，Nb|}KA·（.....................................（¨ ¨{|N b|}KBJ联系我们|Nb|}KB•）.......non={K−1，K−1}）·A B{Na，Nb}见图9。 Needham Schroeder应答器的唯一形状然而，即使是一个令人敬畏的协议，如图8所示的原始Needham-Schroeder协议，也可能具有独特的形状，如图8所示尽管存在图10中描绘的有意跑动和图11中描绘的攻击，但是图10中描绘的意图跑动和图11中描绘的攻击仍然是图9中描绘的。在这里，我们正在研究李约瑟施罗德开始从当地运行的反应器的作用。顺便说一下，注意如果我们从发起人开始，就不会攻击李约瑟·施罗德。也就是说，如果我们假设启动器A完成了一次运行，B的协议，以及私钥K-1和A和B中的-1发生响应者B的匹配运行的情况相反，攻击如图11所示，涉及意图与具有泄露的私钥K-1的某个BJ通信的发起者。因此，我们不认为它是对具有合理密钥保密假设的发起者的攻击。NS形状回想一下，我们是从一个意图回应A的回应者B的角度来考虑李约瑟-施罗德的。让我们假设BA B并且B已经执行了图9中右侧所示的绞合。 在使用¨¨K98S.F. Doghmi等人/理论计算机科学电子笔记173（2007）85非对称加密，私钥仅由接收方用于解构S.F. Doghmi等人/理论计算机科学电子笔记173（2007）8599¨¨¨¨¨初始化响应·{1}|N a，A|}KB）·¨{|N a¨，N b|}KA·（·¨ ¨{|N b|}KB·）·见图10。 Needham Schroeder预期运行{|N a，A|}KBJ（A）P¨¨{|Na，A|}KB• ）B¨ ¨（¨{|N a，Nb|}KA¨·¨{|N b|} Kj• B）P¨¨¨{|N b|}KB·）·见图11。捆绑：对Needham-Schroeder的收到的信息假设在特定的情况下，B接收并发送了这些消息，那么网络中的其他地方一定发生了什么A必须有一个部分匹配的链，消息的发送和接收顺序由两种类型的箭头和连接符号表示≤。这些符号意味着端点是有序的，但其他行为可能会介入，无论是敌对链还是常规链。A或者可以不等于B。没有替代方案：任何包含响应者的图图9的链必须至少包含启动子链的一个实例，事件按所示顺序排列，否则它不可能发生。虽然有一个单一的形状，有两种方式，这种形状可能是在处决中实现或者（1）BJB，因此BJ妥协，在这种情况下，我们可以用对手的活动来完成这个图，以获得Lowe攻击[6];否则（2）BJ=B，导致预期的运行。请注意，形状表示最一般的情况：有一些BJ，我们不知道它是否等于B。有些协议有多个形状。ISO拒绝有两个，正如我们上面看到的奥特韦-里斯有四个。回想一下，当搜索形状时，我们从最初的“骨架”开始，通常只是一个表示分析“观点”的单链。¨100S.F. Doghmi等人/理论计算机科学电子笔记173（2007）85初始化响应{|N a，A|} KB≤{|N a，A|}KB（注：........¨）¨{|N a，Nb|}KA联系我们|N a，Nb|}KA·（.........（¨ ¨{|N b|}KB≤{|N b|}KB·）...）·见图12。Needham Schroeder协议预期运行框架7.2甲醛化由于存在实现任何preskeletonA的同态的无限集合，找到表征所有游程的同态的子集是有用的。表征的概念是为了直观地理解一个方案运行是另一个方案运行的扩展意味着什么在这里，我们抓住了一个扩展的概念，在我们的经验中，我们发现这是最自然和最有用的。定义7.1丛B2扩张丛B1，如果存在原子置换（注意：不一定是内射）α使得B1·α是B2的子丛。 类似地，对于[前]骨架：如果存在替换α使得A1·α是A2的子[前]骨架，则[前]骨架A2扩展[前]骨架A1。自然地将此推广到同态：同态H2：A→A2推广同态H1：A→A1，如果存在原子置换α使得α<$H1：A→A1·α仅仅是H2的余域限制。(i.e.A1·α是A2的子[前]骨架。）这个外延概念可以等价地、更正式地表述如下：定义7.2[前]骨架A2扩展[前]骨架A1当且仅当存在从A1到A2的节点内射同态。同态H2推广了同态H1i ∈H2 =G∈H1，其中G是结点内射同态。例7.3图7.3中Needham Schroeder应答者的预期运行骨架。12延伸图11中描绘的形状9 .第九条。现在我们可以定义一组协议运行（已实现的同态/骨架）是A的特征化意味着什么。定义7.4同态的集合X是A的一个特征，如果. 每个H∈X实现A. 每个实现A的同态HJ扩张某个H∈X我们也可以把A的一个刻画看作是一组已实现的骨架（同态的余域然而，把一个刻画看作是一组从A实现的同态更能提供信息，因为它具体说明了A如何S.F. Doghmi等人/理论计算机科学电子笔记173（2007）85101是协议运行的一部分我们可以称之为“刻画中的骨架”，在这种情况下，我们指的是刻画中同态的余域。显然，A的所有实现同态的集合是A的一个特征。然而，我们寻求一个尽可能小的特征：一个最小的特征，在一些标准的大小（节点数，消息的总大小...等等）。稍后我们将证明，对于所有这些尺寸定义，存在一个唯一的最小值。上面描述的扩展概念捕捉了一个协议运行仅仅是另一个运行的细化的含义我们可以对extends的几个替代概念进行论证，包括在上面的定义7.2中不要求G的节点内射性，和/或要求G的原子内射性。这些定义中的任何一个都将产生可用于决定安全谓词的特征。然而，它们在大小、算法构造的难易程度以及分析师解释所有运行集并根据它们做出判断的难易程度上有所不同。我们选择这个概念的扩展基于我们的经验，在自动化协议分析，我们发现，最低的characterizations，它产生简洁地捕捉直观的概念在我们的extends定义中要求节点内射性还有另一个好处，因为它导致了一个偏序而不是一个预序。此外，偏序是有根据的。定义7.5对于骨架，A1≤nA2i ∈A2是A1的延伸。同样地，对于同态，H1≤nH2i<$H2扩张H1.命题7.6 ≤ n是骨架上的良基偏序（直到同构）。证据显然，≤n是自反的和传递的。反对称：如果A≤nAJviaH = [φ，α]和AJ≤nAviaHJ，则两者具有相同的节点数。通过考虑H和HJ的合成，我们可以看到H是节点双射（φ是双射）和原子双射（α是双射）。通过考虑H和HJ的合成，我们还可以看到α是从非A到非AJ的双射，也是从唯一A到唯一AJ的双射。同样地，φ是从≤A到≤AJ。因此H−1=[φ−1，α−1]是一个同态，是H的逆。H是同构的。适基性：对于骨架A，设Occ（A）为骨架A中原子的个数。设Atoms（A）是A中不同原子的数量，并将骨架的原子冗余定义为red（A）=Occ（A）-Atoms（A）。另外，设nonOcc（A）和uniqOcc（A）分别是非 A和唯一 A中原子在A我们可以证明|节点|、红色、nonOcc、uniqOcc和| ≤ |每个都是非递减的，≤n，下限为0。让等级（A）=|节点A|+ red（A）+nonOcc（A）+uniqOcc（A）+ |≤A|102S.F. Doghmi等人/理论计算机科学电子笔记173（2007）85骨架的秩是不减的，≤n，下界为0。进一步，注意如果A ≤nAJ，且Rank（A）=Rank（AJ），则A和AJ必须同构。因此，≤n在同构上是良基的。Q这类似地延伸到同态。推论7.7≤n是同态（直到同构）上的良基偏序我们将把形定义为在这个良基偏序中的最小实现同态定义7.8一个同态H是A的一个形状，如果H实现A，并且H在≤n下是实现A的同态中的最小同态。设shapes（A）是A的不同（直到同构）形状的集合。接下来，变得明显的是，A的形状集合描述（可以扩展到）与A兼容的所有运行命题7.9形状（A）是A的一个特征证据由于≤n是良基的，对任意实现A的HJ，存在H∈shapes（A）使得H≤NHJ，且HJ是H的扩张.Q实际上，形状的集合是这样的集合命题7.10形状（A）是A的任何其他特征的子集。因此，形状（A）是A的最小特征。证据 取任何其他的表征X为A。取任意形状H∈shapes（A）。由于X是一个特征，所以一定存在某个G∈X使得G≤nH.由于H在≤n下极小，则G H。Q从7.10我们可以看到，形状（A）是在大多数大小定义（节点数，消息总长度......）下A的最小特征等等）。8结论和今后的工作在形状集是有限的情况下，preskeletonA的形状形成了所有与A兼容的协议运行的简洁表示。在我们研究过的大多数协议然而，确定保证这一点的协议的子类将是有用的我们期望类似于[1]和[8]中定义的协议的子类具有此属性。我们还开发了一个算法，在[2]中讨论，用于构建Preskeleton的形状集。在高层次上，该算法从初始preskeleton开始，找到并解决认证测试（见[4]），以产生一组有限的解同态/preskeleton，然后在这些上递归这个结果是一个S.F. Doghmi等人/理论计算机科学电子笔记173（2007）85103一种叶子形状类似的圣诞树这些形状被标注了保密信息。该算法通过尝试构造一个形状来揭示一个值来推理保密性。该算法的性能的进一步分析将是未来工作的主题。引用[1] 布鲁诺·布兰切特和安德烈亚斯·波德斯基。加密协议的验证：标记强制终止。在Andrew D. Gordon，编辑，软件科学和计算结构基础，LNCS第2620期，第136-152页。Springer，2003年4月。[2] 沙丁湾作者：Joshua D. Guttman和F. 哈维尔·塞尔在加密协议中搜索形状。系统构造与分析的工具与算法（TACAS），LNCS。Springer，2007年3月。扩展版网址：http://eprint.iacr.org/2006/435。[3] 约书亚·D古特曼安全目标：数据包轨迹和串空间。在Roberto Gorrieri和Riccardo Focardi，编辑，安全分析和设计的基础，LNCS第2171卷，第197-261页。Springer Verlag，2001年。[4] 约书亚·DGuttman和F.哈维尔·塞尔验证测试和捆绑包的结构理论计算机科学，283（2）：333[5] 约书亚·DGuttman，F.Javi
我的内容管理
展开
