密码协议的形式验证.doc

密码协议的形式验证摘要：无线通信在设计合适的安全协议方面，设置了一定数量的限制。导致了着重于无线应用的新协议诞生。其中的一些协议缺点明显。形式验证是是增加安全协议的信赖所必不可少的部分。本文将讨论形式验证的不同方法。以一个针对无线通信的安全协议，运用一个逻辑模型来表示的形式确认作为例子。关键词：安全协议，协议确认，确认逻辑，认证，移动安全1. 绪论无线通信为安全协议的设计设置了一些限制。用于这类通信的移动设备，通常只有限的计算和储存能力。况且，用户和网络之间的带宽通常是限定的；因此通过无线电接口发送的信息必须保持最小值。由于这些约束，以及其它需要注意的方面如匿名，所以常规的协议不适于无线通信。导致一些着重于无线应用的新协议诞生。包括ASK协议1，ASPeCT协议2和Wong-Chan协议3。一些其他的候选的认证协议如最近Park4和Yietal提出的协议，已经被发现了很多缺点67。已经发布的协议所存在的缺点，表明了源协议的设计是非常复杂和容易出错的过程。已经证明非正式技术在协议验证方面的不足。正式的验证技术提供了一种提高协议安全的手段。这种技术强制执行了最初设想的明确规范以及协议的目标，因此协议范围的定义。而且，由于这个方法的本质，以系统性的方式发现协议的弱点。但是检测弱点的能力与所用技术的限制相关的。本文讨论形式验证的不同方法。大概的方法包括状态机，代数项重写技术，定理证明技术和逻辑模型。而且，通过逻辑基础技术证明形式确认的进程是一项安全的协议。本文着重于形式确认的优点，并鼓励推广这项技术。2. 形式协议确认形式证明是确保密码协议安全的必要步骤。一些技术可以用来分析协议的安全性。包括状态机，代数项重写技术，定理证明技术和逻辑模型。2.1. 状态机状态机运用一项可达性分析技术8的方法分析协议。运用这项协议，系统的全局状态由每一个过渡表示。然后分析每一个全局状态是否发现有状态协议上的错误导致攻击者获得了访问保密信息权限。一个详细的研究证实了所有可达到状态都是安全的。可达性分析适于判别一个协议是否匹配其规格，但并不保证被主动袭击时动安全性。这项其它的一系列限制是需要通过极端的假定来保持较小的状态空间9。一些状态机并没有明确针对安全协议分析的设计。这些工具10的一个问题在于不能辨别安全领域内细微的缺陷，如应对攻击。特别针对协议分析设计的工具可以应对攻击，但会受限于所有状态机的影响。基于纯状态空间研究的方法可以判别一个协议是否包含了一个已经定义的缺陷，却不太可能发现协议中不明种类的缺陷。由于有这些缺陷的存在，所以即便基于状态机的技术可以与其他技术高效率地结合，却是永远也不能取代其他的验证技术。状态机的研究效率低下，经常不确定（由于空间太大而不能分析）和不能找出新的错误；因此协议设计人员很少使用。2.2. 代数项重写技术代数项重写技术与状态机非常相像。但是状态机技术由不安全的状态开始，试图表明不存在从原始状态通向不安全状态的路径。与之相比，代数项重写技术适于初始的状态规格。努力证明不能到达不安全状态。尽管代数项重写技术与所有的方法有关，由于可以发现新协议的缺点，所以还是比常规状态机有所发展。但是这项技术始终受一系列的限制。一个问题是只考虑已经被系统描述的行为。合理地使用并没有充分代表入侵者发出的信息。可以考虑窃听与回应攻击，但当入侵者采用新信息时，这项技术便失败了。代数项重写的另一个问题就是复杂，这减轻了它对程序设计人员的吸引。2.3. 原理证明技术手工生产证明是很难生产的。针对原理证明用来协助数学命题的证明的工具已经被开发出来。在用户知道每一个阶段的证明下，这些程序允许一步一步地进入和证明数学陈述。因为一个安全协议可以被精确指定，精确无误的公式可以被定义，给定协议的在设定情景是安全的状态能用精确的数学项解释。这种陈述能够进入一个原理证明而证明的研究也可以进行。然而，原理的证明方法在展示协议的正确性方面比找出协议被攻击的漏洞方面做得好。况且，一个原理证明要求用户通过证明找出正确合理直观可行的路径。因此源程序的验证有可能由于操作者缺乏经验而失败。尽管有诸多限制，原理证明还是对协议设计人员有利的，尤其是与其他技术融合的时候。2.4. 模型逻辑运用逻辑的安全协议形式验证在以前被认为是安全的协议中发现了一些缺陷1112。逻辑技术涉及演绎推理的进程，在其中所希望的协议目标是通过对假定应用一些公理和推导规则来演绎，以及通知协议的交换12。接下来的一节以GNY逻辑为例，描述了基于协议验证的逻辑方法。2.4.1. GNY逻辑Gong，Needham和Yahalom11的逻辑通常称为GNY逻辑。GNY逻辑是用作正式的验证密码协议。表一为本文中所用GNY的构成，更多的细节和完全的描述参阅11。用GNY逻辑验证一个协议，必须进行一下步骤：1. 协议形式化2. 初始假定说明3. 协议目标说明4. 应用逻辑假定尽管GNY非常有效，但还是存在限制：不包含短期操作者，仅仅按信条处理而不是按所知，用依靠人解释的理想化的规则。然而，阻碍GNY普及的更严重的问题是它的复杂。两个公式级联和对称加密和解密公共密钥加密和解密个人密钥加密和解密公式X是新的，在运行协议之前没有被发送过公式X是可识别的P告诉X。P接收了包含X的信息，P能读和重复XP告诉X，在当前协议运行中不要通过P转达P拥有或有能力拥有公式XP传递XP相信X，即P的主要行为都是假定X是真的信息X含C的拓展。X转送的先决条件是被C陈述所代表P管辖X。对于X来说原则P是权威值得信赖K是P和Q相适应的秘密。它们可以使用K（或者K的推导）作为通信的密钥或者身份的证明表一 GNY逻辑的使用子集3. ASK协议和它的验证无线通信为设计合适的安全协议设置了一些限制。用于通信的移动设备通常都只有有限的运算和储存能力。而且用户和网络之间的通信带宽是有限制的；因此通过无线电接口发布的信息必须保持最小。由于这些限制和其它问题如匿名，所以常规的协议不适于无线通信。于是就提出了着重于无线应用的新协议。包括ASK协议1，ASPeCT2协议和Wong-Chan协议3。本文描述这些协议的符号如表二所示。U用户鉴别V服务提供者鉴别S证书核查鉴别KK一个关键的加密密钥SK会议密钥rX一个由X生成的随机数表二 协议术语3.1. ASK协议ASK协议1首先使用椭圆曲线加密以达到“认证和密钥确认”。因为在不同通信端的计算负担是不对称的，所以这项技术尤其适合于无线通信。所以在移动设备上的计算要求很低。椭圆曲线加密的更大的优点是密钥尺寸小。与基于常规公共密钥加密系统的协议相比，减小了带宽要求。ASK协议的信息交换如图一所示。ASK协议的前两个步骤，主要是主体交换公共密钥。在这个阶段用个人密钥通过加密其它主体的公共密钥，每个主体可以计算关键的加密密钥KK，即进行了Diffie-Hellman密钥交换。然后服务提供者V生成随机数rV，可以用KK加密来生产会议密钥SK。接着V给用户U发一条信息，包含了随机数rV和它的用KK加密的证书。用户U在收到rV之后，可以算出会议密钥。U也可以通过测试证书，验证之前收到属于V的公共密钥。协议以一条从用户发送给服务提供者的信息结束，其中包含了用户的证书和由前些时候V生成的随机数。这条信息要求实现用户认证。尽管协议明显简单，可是ASK协议的缺点也已经被发现6。本文中ASK协议的形式验证表明了GNY逻辑检测弱点的能力，因此在释放它们进入公共域之前应强调安全协议的形式验证的重要性。3.2. ASK协议的验证这一节将应用GNY逻辑验证ASK协议3.2.1. 协议公式化3.2.2. 初始设想的规格3.2.3. 协议目标的规格3.2.4. 逻辑假设的应用ASK1：- 公理T1推断- 运用公理P1推出：- 因为，根据P8，U可以计算出，因此ASK2：- 公理T1推断- 运用公理P1推出：- 因为，根据P8， - 而且，因为，由公理2得- 由公理F1，因为，得- 因为Diffie-Hellman密钥交换依赖于底层加密系统，所以GNY逻辑不能驱动。为了继续证明，有以下假定：关键加密密钥KK由Diffie-Hellman密钥交换所建立。因此可以考虑分享预计和主体之间的机密。只有这些主体可以生成会议密钥，因为关键加密密钥是不可缺少的先决条件。因此我们能假定。也就是说V相信SK适合分享机密。ASK3: - 原理T1推断- 因为，通过公理T3，可以解密信息和告知信息内容。公理T2和P1推断U拥有每个部分的信息- 因此，。因为ASK1有，公理P2推断- 因为Diffie-Hellman密钥交换依赖于底层加密系统，所以GNY逻辑不能驱动。为了继续证明，由ASK2，可以假定 。也就是U相信SK适于分享机密- 因此，实现了U的密钥承认。但是U不能建立新密钥- 因为证书认证签署了CertV，可以应用公理I4，推出。通过公理T6，T2和P1，U可以通过CertV得到V的公共密钥- U相信S足够诚实值得信赖并且传送了CertV。通过证书认证所提供的撤销名单和到期时间，U可以建立CertV的有效性。因为信任仅仅在V的个人密钥建立，所以可以认为CertV足够的新。因此可以应用公理J2得出- 因为U相信S对V的公共密钥有管辖权，公理J1可推出- U承认CertV，因此公理R1推出U承认完整的信息ASK3- 在这一阶段，协议失败了，因为不能推出，导致了接下来协议的失败。首先新鲜度信任是一个目标。其次公理I1的先决条件要求推出以及。因此不能通过协议提供V到U的认证。ASK4: - 公理T1推出- 因为，有公理T3可以解密信息和告知信息内容。公理T2和P1推出V拥信息的每个部分- V相信S足够诚实值得信赖并且传送了CertU。通过证书认证所提供的撤销名单和到期时间，V可以建立CertU的有效性。因为信任仅仅在U的个人密钥建立，所以可以认为CertV足够的新。因此可以应用公理J2得出- 因为V相信S对U的公共密钥有管辖权，公理J1可推出- V承认CertU，因此公理R1推出V承认完整的信息ASK4- 因为公理F1推出，完成了公理I1所有的先决条件，可以推出，完成了U对V的验证- I6的应用得到，从P3，可以推出。应用P2得到ASK协议标准证明完成了。三个设想的目标不能证明。第一个是关于在会议密钥的新鲜度上对于U的信任：。这个目标的失败非常关键，因为U不能侦查到回馈的信息，从而导致了重新使用旧的会议密钥。这就可能被已知密钥攻击所利用。第二和第三个失败的目标是U对ASK3信息新鲜度的信任：。以及U对V传送ASK3的信任：。因为信息ASK3不能回复旧的信息，所以这些失败使得V对U的认证不能实现。因此攻击者可以伪装成服务提供者。然而，没有相应的会议密钥，受到的攻击就不会很严重，因为攻击者不能参与接下来的通信。但是，如果攻击者知道了以前的会议密钥（已知密钥攻击），就可以通过简单回复旧信息伪装成服务提供者。3.3. GNY逻辑的局限在以上协议分析的纲要之中，出现了几种GNY逻辑的局限。最显著的局限是没有共享机密模型推导的能力和只有两个时间段。因为无线网络协议使用公共/个人密钥对来推导共享机密，所以在共享机密的推导上的限制是很明显的。例如Diffie-Hellman密钥交换，两方面都用个人密钥加密对方的公共密钥而得出一个对称密钥。但是这一技术依赖于底层加密系统，通用的逻辑不能包含处理这种技术的原理。因此非正式推理用来推导不能被逻辑推出的猜想。时间上的限制使得不同程度的新鲜度难于区分。例如一个随机数的新鲜度表明它没有在之前运行的其它协议中使用过。另一方面，为了通过逻辑证实过于公共密钥的猜想，证书必须足够新鲜。然而证书的新鲜度仅仅意味着当时人可以证实证书的有效性。这经常通过包含在证书里面的到期时间和公布不可用证书的废除清单实现。需要注意到，一个猜想证书是当前（即可以）的实体没有理由相信整条信息及其组件是新鲜的。3.4. 固定ASK协议本节提出了一种新的为了实现认证和密钥协议的ASK协议交换。其中设立了一个由用户生成包含在第二或第三条信息的随机值。这个值也是用来推导会议密钥的。新提议大纲如图二所示。大纲按着新协议的形式验证。因为大部分的证明与ASK协议的证明一样，所以这里只给出不同的部分。3.4.1. 协议公式化3.4.2. 初始假定规格与ASK协议验证的假定一样。两个假定都需要和3.4.3. 协议目标规格由原来的目标变成了现在的，而变成了现在的，其他所有目标与ASK协议验证相同。3.4.4. 逻辑假设应用ASK1：与原始ASK协议的验证相同。ASK2：- 公理P1推断- 因为，根据P8， - 而且，因为，由公理2得ASK3: - 因为，通过公理T3，可以解密信息和告知信息内容。公理T2和P1推断U拥有每个部分的信息- 因此，。因为ASK1有，公理P2推断- 因为，从公理F1推出- 因为，从公理F1推出，又因为，故从公理F2推出- 因为证书认证签署了CertV，可以应用公理I4，推出。通过公理T6，T2和P1，U可以通过CertV得到V的公共密钥- U承认CertV，因此公理R1推出U承认完整的信息ASK3。这就满足了公理I1的所有先决条件，可以推出和。因此协议提供了V到U的认证。ASK4: 与原始ASK协议的验证相同。以上所有协议目标声明新协议的验证都已被推导。因此，新协议在其应用范围和逻辑限制内可以被认为是安全的。4. 总结本文讨论形式验证的不同方法。大概的方法包括状态机，代数项重写技术，定理证明技术和