《三方认证密钥协商协议形式化安全模型的分析与改进.doc》由会员分享，可在线阅读，更多相关《三方认证密钥协商协议形式化安全模型的分析与改进.doc（12页珍藏版）》请在三一办公上搜索。
1、三方认证密钥协商协议形式化安全模型的分析与改进摘 要：本文对两个三方认证密钥协商协议的形式化安全模型扩展BR模型和扩展CK模型进行了分析，发现了扩展BR模型中在三方身份认证方面存在的安全漏洞，指出了扩展CK模型中匹配会话定义的局限性，并根据802.11i所规范的协议流程，通过引入有效的概念，提出了三方认证密钥协商协议改进的形式化安全模型，并在该模型下证明了改进后EAP-TLS协议的安全性。新模型为解决无线局域网等特定环境下认证密钥协商协议的安全性问题提供了较好的解决思路。关键词：802.11i；EAP协议；可证明安全性；三方形式化安全模型1 引言2004年IEEE 802.11标准组提出了80
2、2.11i标准以增强无线局域网的安全性能。在该标准中，客户端的认证和接入控制功能是通过802.1X协议实现的，而802.1X协议的认证功能是通过上层认证协议EAP完成的，因此对EAP协议的安全性进行研究就显得十分重要。然而，目前针对802.11i的三方认证协议研究还没有完善的形式化安全模型，1995年Bellare等人提出了三方密钥交换的形式化安全模型，但此模型没有考虑实体间的认证关系。2008年曹春杰提出了扩展的CK模型，给出了三方认证密钥协商协议的形式化模型，但该模型中关于接入点会话标识符的定义因为存在不确定性而并不实用（事实上文献3中也并没有给出具体的协议并利用该模型进行证明）。2010
3、年宋宇波等人提出了扩展的BR模型，该模型利用参与方产生的会话序列对匹配会话进行定义，但由于没有考虑接入点在一次协议中产生的两条会话序列之间的关系，因而该定义有可能会导致三方消息认证不安全。因此，如何对三方认证密钥协商协议的形式化安全模型进行改进与完善，使其能保证无线局域网的参与方可以进行安全认证还需要进一步的深入研究。本文通过对现有三方认证密钥协商协议形式化模型进行深入分析，指出利用匹配会话定义三方协议的认证关系时需要考虑特定的应用背景，这是因为交互的三方中至少有一方要与其它两方同时进行消息交互，对于这一方的会话描述（无论是用会话序列或是会话标识符）必须考虑其自身所处的网络位置和所具备的网络功
4、能，否则一旦攻击者对该方进行冒充或破坏，就可能造成匹配会话定义的失效。对于802.11i而言，作为和中间具有转发功能的参与方，其与和的交互内容有一定的重复性，本文根据这一重要特点，在改进的形式化安全模型中给出会话标识符有效的定义。802.11i协议流程如图1所示：图1 802.11i协议流程客户端通过无线网络与接入点进行连接，通过有线网络与认证服务器进行连接，的功能是接收消息后进行加脱密操作并转发消息，的功能是对进行认证。802.11i协议中和通过转发响应各自的身份、加密方式、公钥等相关信息，然后由发起EAP认证协议。设有一对公私钥，有一对公私钥，与间共享长期对称密钥。EAP-TLS协议的目的
5、是通过一系列的交互使客户端与认证服务器间协商主会话密钥，并实现相互的身份认证。EAP协议完成后将协商得到的通过加密的方式发送给。然后与利用进一步完成四步握手协议。在本文中，三方认证密钥协商协议指EAP协议，由于EAP是完成认证和主会话密钥协商的核心步骤，所以改进的形式化安全模型也是建立在802.11i所规范的EAP环节上。2 现有三方认证密钥协商协议安全模型分析本节我们简要回顾文献4和文献3中提出的扩展BR模型和扩展CK模型。通过分析发现，扩展的BR模型中关于匹配会话的定义可能会导致消息认证不安全，不能抵抗攻击者对的冒充攻击。在扩展的CK模型中，当攻击者冒充时会导致会话标识符定义的失效。2.1
6、 扩展BR模型及安全性分析文献4中扩展BR模型将三方认证密钥协商协议形式化为一个四元组来描述。其中，定义了一个诚实客户端的会话行为，定义了一个诚实接入点的会话行为，定义为诚实认证服务器的会话行为，为认证服务器分发给客户端和无线接入点的初始会话密钥。该模型将攻击者形式化为拥有黑盒预言机、和的概率图灵机，且可以对这些预言机进行预定的查询并从预言机那里获得应答。 为了描述参与方之间的认证关系，文献4在原BR模型两方认证安全的基础上进行了扩展。在原BR模型中，若两条会话序列分别是对方的匹配会话，则称这两条会话序列是匹配会话。在扩展BR模型中，这种匹配会话的定义被直接推广到了三方的情况：设预言机为、以及
7、，产生的相应会话序列分别用和表示，则在扩展BR模型中，三方之间的匹配会话和消息认证安全的定义如下：定义1 如果是的匹配会话，也是的匹配会话；是的匹配会话，也是的匹配会话，则称预言机之间有匹配的会话。当一个协议在攻击者的控制下执行，如果存在一个没有被攻破的预言机呈接受状态，但没有一个与它有匹配会话的预言机存在的时候，称这样的会话是不匹配的。定义2 如果不匹配会话的概率是可忽略的，则称协议是消息认证安全的。定义1分别给出了与，与之间会话的匹配关系，但是却忽略了这两者之间的相关性，也就是说攻击者可以通过重放某次协议中的一个匹配关系构造出满足定义1的匹配会话使三方都接受。因此通过上述匹配会话给出的认证
8、安全的定义2至多只能提供和，和之间的认证，却不能保证与之间的认证，这样就不能实现802.11i中EAP-TLS协议的目的(提供客户端和认证服务器的双向认证)。为了便于说明举例如下： ( 1 ) 是协议的合法参与方，与正常的，进行一次会话后得到匹配会话，。 ( 2 ) 是攻击者，通过重放(1)中的会话与正常的，进行一次会话后得到相应的会话，。由于，是匹配会话，是与完成的一次正常交互，因此同样是匹配会话，那么根据定义1有，是一个匹配会话，但此时，均认为攻击者的正确身份是。这说明在文献4中扩展的BR模型关于消息认证安全的定义有一定的局域性，为了避免因此造成的安全漏洞，有必要对其进行改进。2.2 扩展
9、CK模型的定义缺陷2008年曹春杰基于CK模型，提出了支持三方协议的形式化安全模型扩展CK模型。该模型通过会话标识符来定义匹配会话。定义3 令为会话标识符，为协议参与方的身份，为参与方在协议中的角色。设在三方认证协议的一次执行中，生成会话 ，生成会话，生成，如果有，且互不相同，则我们称这三个会话是匹配会话。利用会话标识符定义匹配会话比通过会话序列定义更简洁有效。但该模型与CK模型一样，并没有给出的具体定义，只是简单地将两方的情况推广至三方，而没有考虑定义的存在性和确定性。扩展的CK模型同样是基于无线局域网而设计的。该模型假设协议正常执行的情况下，包括敌手在内的任意会话在执行后都生成相应的，并基
10、于此定义匹配会话。但我们通过分析发现，当攻击者对进行冒充时可能造成会话标识符具有不确定性，如下例所示： 假设敌手通过消息重放等手段完成了以上会话实例，按照定义和分别生成会话标识符， 。由于协议执行中涉及接收并发送多个不同消息(，)，因而此时对会话标识符的定义可以有多种选择，例如可以设或，这就造成定义具有不确定性。而事实上，的作用是对协议的某一次会话做特定的标识，应当具有唯一性，因此在上述情况下，扩展CK模型关于匹配会话的定义显然是不合理的。为了解决上述问题，需对802.11i的协议流程进行进一步分析，根据的功能对会话标识符定义进一步完善。3 改进的三方认证密钥协商协议形式化安全模型我们在对扩展
11、BR模型和扩展CK模型分析的基础上，提出了改进的三方认证密钥协商协议形式化安全模型。该模型充分考虑了的功能和特点，通过引入有效的概念，解决了三方身份认证中匹配会话定义不完善和不确定的问题。在该模型下可证安全的三方EAP协议可以实现与的交互认证且能保证主会话密钥安全，因而对802.11i中EAP协议的设计与分析有着重要的意义，对该模型的详细描述如下：3.1 敌手能力由于802.11i协议中的认证环节是采用完整的加密或签名算法来实现的，所以新模型并不适合假设敌手可以通过某种方法得到参与者的长期密钥或者临时密钥，因为这种假设会直接导致敌手对用户消息的签名伪造或者加脱密。在本模型中对敌手的攻击能力假设
12、如下。、分别拥有自己的公私钥对，此外、之间共享一对长期对称密钥。攻击者可以窃听、篡改、转发、删除、伪造、嵌入三方之间交互的消息，具体地可以将敌手能力形式化为以下对预言机的查询：查询：攻击者可以对、进行查询。当进行查询时，返回参与方的第次会话的会话实例。此查询模拟被动攻击，即敌手具有获得大量会话实例的能力。查询：攻击者可以对、进行查询。当进行查询时，攻击者发送消息给参与方的第次会话，根据协议的约定执行，并返回给敌手相应的执行结果。此询问模拟主动攻击，描述敌手进行消息的伪造、重放、篡改等对消息进行修改操作的能力。在802.11i所规范的协议流程中，和协商生成主会话密钥，并由将加密后发送给。为了使模
13、型简单且易于分析，可以合理的假设的安全性仅依赖于认证协议的安全性，对于将加密后发送给这一步骤并不计算在认证密钥协商协议中，且认为其不泄露的任何信息。因此对查询定义如下：查询：攻击者可以对和的会话进行查询，当进行查询时，(或)所对应的会话实例返回给攻击者本次会话生成的会话密钥。此攻击形式化了敌手进行相关密钥攻击的能力。查询：攻击者只能对没有被进行过查询且已经完成的或的会话进行Test询问。敌手进行一次随机掷币，如果掷币结果b=0，则返回给敌手；如果b=1，则返回给敌手一个随机数（取自主会话密钥空间），但敌手不知道掷币的结果，他根据返回值做判断，输出，用表示敌手猜对的概率，用表示敌手的优势，根据不
14、可区分性理论，如果的值是可忽略，那么敌手不能得到会话密钥的任何信息。我们称具有上述4种能力的敌手为3AKE敌手。上述对敌手的形式化描述仅限于此三方协议是利用加脱密算法和签名算法进行设计的情况，因此不适合假设敌手具有很强的攻击能力。但是如果在此模型下的协议是利用困难问题进行设计的，则可以进一步考虑敌手得到长期密钥和临时密钥的能力，从而得到基于ECK2007模型的三方扩展模型。3.2 安全性定义在对扩展BR模型分析后发现，通过交互消息产生的会话序列来定义匹配会话具有一定的局域性，这是因为在三方协议中，在与进行消息交互的同时也与进行消息交互，所以会话序列很难将与另两方的会话都刻画清楚，因此在改进的模
15、型中我们通过会话标识符来定义匹配会话。由于的功能主要是消息的加脱密和转发，这意味着会话(1)中的，的消息内容有着明显的关联和重复性，我们可以利用这种关联引入有效的概念，通过有效将与、与之间的会话联系起来，进而给出三方匹配会话的定义。定义4 设与之间共享密钥、加密算法和相应的脱密算法，如果在时刻，接收到来自的消息，在紧邻的下一个时刻发送给消息，在时刻接收到来自的消息，在紧邻的下一个时刻发送给消息，且有，则称是有效的。会话标识符是协议参与方在接受后生成的用于标记此次会话的标识，具体定义为参与方执行过程中接收和发送消息内容的串接。不妨设参与方、接受后生成的会话标识符为，其中与的会话标识符与CK模型类
16、似，对于执行过程中重复出现的消息内容仅在计算在此次会话的时使用一次。根据上述定义可以得到如下性质。性质1 对于一次正确会话的参与方、，在协议完成后分别生成相应的会话标识符，如果是有效的，则有。证明 设为与会话消息的串接。如果协议执行过程中没有攻击者的参与，且各方都顺利完成了会话过程，（即是正确会话），那么有。由有效性的定义可知，其中为与交互的消息内容，据此可以定义的会话标识符。同理可知，当协议正确执行时有，于是性质1成立。性质2 对于不是有效参与的协议会话，在全部接受后生成会话标识符，则必然有。证明 若不是有效的由定义可知，所以或，不妨设，因为在某个时刻，接收到消息，则必然在时刻由发送过消息，
17、所以中包含；如果在某个时刻，发送过消息，则必然在时刻由接收到消息，所以中包含，由可知。以下给出改进后安全模型下关于匹配会话和认证密钥协商安全的定义：定义5 如果对有效的参与的会话在执行后，参与的三方都接受会话且生成的会话标识符，则称是匹配会话。定义6 称802.11i规范下的EAP-TLS协议是三方认证安全的，如果该协议满足以下三条：(1)如果是匹配会话，则对应的都接受；(2)如果都接受，则是匹配会话；(3)对于无效参与的协议，不存在会话使或接受。定义7 称802.11i规范下的EAP-TLS协议是安全的，如果对任意3AKE敌手满足以下两条：(1)协议执行后、生成相同的；(2)敌手优势是可忽略
18、的。4 EAP-TLS协议及其安全证明为进一步验证改进后安全模型的有效性和合理性，我们提出一个适用于802.11i的新EAP-TLS协议，并利用所提出的新三方认证密钥协商形式化安全模型对其进行证明。 新的EAP-TLS协议协议的执行过程如下：收到EAP-Start请求后，随机生成并发送给，对进行加密后转发给；由密钥空间中随机生成利用加密后与一起进行签名，将签名后的结果加密后发送给，脱密后转发给；对签名进行验证(检查是否相等)，并利用自己的私钥对脱密得到，对进行杂凑并用自己的私钥签名后发送给，然后接受，随后加密转发给；对进行脱密操作后对进行杂凑并验证其是否为签名内容，若验证通过接受。和协商得主会
19、话密钥， 。定理1 如果签名算法是不可伪造的，则上述协议是三方认证安全的。证明 只需要证明上述新EAP-TLS协议满足定义6中的三条即可。对于定义的第一条易知在协议正常执行的情况下，满足有效性的定义，此时若是匹配会话，则由性质1有，显然三方都会接受。下面我们证明协议满足定义6的第二条：对于有效参与的协议，要使三方都接受，则中一定包含消息使得接受。同样对于认证服务器，中一定包含消息使接受。由于签名算法是不可伪造的，所以攻击者不可能构造出这样的签名，则这两个签名必然是由转发的，这说明曾接收到消息和。又由长期密钥的保密性和签名算法的安全性可知，攻击者同样不能对这两条消息进行伪造，因此曾发送过消息，曾
20、发送过消息。综上所述，各包含的消息如下：包含消息、；包含消息、；包含消息、，因此有，于是是匹配会话。最后我们证明当参与协议的非有效时，不存在会话使三方都接受。利用反证法不妨假设存在会话使三方都接受，则接受后的会话生成相应的会话标识符 ，由性质2可知，当非有效时有，则必然有或者是。对于前一种情况意味着攻击者可以对认证服务器的签名进行伪造，第二种情况意味着攻击者可以对的签名进行伪造，这显然与签名算法的安全性相矛盾，因此该协议满足三方认证安全定义的三个条件。定理2 如果杂凑函数是安全的，加密算法和是安全的，签名算法是不可伪造的，则上述协议是安全的。证明 设攻击者进行查询后猜测掷币结果成功的概率为，我
21、们分别对敌手三种不同的攻击方式构造区分器。(1)查询：假设攻击者可以进行次查询，用表示敌手利用此类查询猜测成功的概率。攻击者利用此查询获得关于信息的有效方式是通过和来进行计算的，我们对此做如下实验。实验1：挑战者进行一次随机掷币，若结果为则返回给攻击者，若结果为则随机选择(为空间)返回给攻击者，攻击者根据返回的结果猜测挑战者掷币的结果为，令表示攻击者猜测正确的概率。实验2：挑战者进行一次随机掷币，若结果为则返回给攻击者，若结果为则随机选择(为空间)返回给攻击者，攻击者根据返回的结果猜测挑战者掷币的结果为，令表示攻击者猜测正确的概率。在实验1中，由于算法是安全的，攻击者至多进行次查询，则敌手通过
22、此查询赢得实验1的概率。同理在实验2中，由于杂凑函数是安全的，因此敌手通过查询赢得实验2的概率，因此=+待添加的隐藏文字内容3(2)查询：假设攻击者可以进行次查询，用表示敌手利用此查询猜测成功的概率。事实上，攻击者能否利用查询得到的信息等同于攻击者能否对签名进行伪造。因此我们构造攻击者对签名的伪造实验：实验：对于给定的参数，查询做出后，攻击者随机生成，并由的密钥空间中随机选择，构造签名 ，由于攻击者至多进行次查询，不妨假设攻击者利用此方法构造了一个具有个签名的列表：在实验中，如果第次查询的签名属于列表，则返回给攻击者相应的主会话密钥，否则返回“”。实验：同实验类似，查询做出后，攻击者随机生成，
23、并由的密钥空间中随机选择，构造签名 ，由于攻击者至多进行次查询，不妨假设攻击者利用此方法构造了一个具有个签名的列表：.在实验中，如果第次查询的签名属于列表，则返回给攻击者相应的主会话密钥，否则返回“”。设和的密钥空间为，则攻击者利用实验1伪造成功的概率为，利用实验2伪造成功的概率为，因此=+(3)查询：设攻击者可以对当前攻击实例外的其它个会话实例进行查询，返回给攻击者被查询会话生成的主会话密钥。由于每次会话的都随机独立的选取，因此攻击者利用此查询猜测查询掷币结果成功的概率。综上所述，攻击者对查询掷币结果猜测成功的概率=+因此该协议是安全的。 5 小结本文在802.11i的协议规范下，根据所具有
24、的特定功能和实际应用中的一些特点，给出了有效的概念，并利用其给出了此类模型的两个基本性质。并通过将其应用于具体的EAP-TLS协议的安全性证明中，说明了该模型具有一定的合理性和适用性。本文所提出的三方模型主要考虑了无线局域网这一特定的应用背景，对于其它三方环境并未做细致的研究。在下一步工作中，可以针对其它有特定应用背景的三方协议对形式化安全模型进一步研究，并可以假设敌手具有更强的攻击能力来建立新的模型，在此类新模型下，可以利用数学困难问题设计更高效的安全认证密钥协商协议。参考文献1 IEEE802.11i. IEEE Standard for information technology-Te
25、lecommunications and inform ation exchange between systems-Local and metropolitan area networks-Specific requirements part 1 1：Wireless LAN Medium Access control(MAC) and Physical Layer(PHY)specifications: Medium Access Control(MAC) SecurityEnhancementsS. America,ISO/IEC,2004:1341.2 M Bellare and P
26、Rogaway. Provably Secure Session Key Distribution-The Three Party CaseA. Proc.Annual Symposium on the Theory of ComputingC.ACM,2005:5766.3 曹春杰.可证明安全的认证及密钥交换协议设计与分析.西安电子科技大学博士学位论文.2008. 4 宋宇波,胡爱群,姚冰心. 802.1li认证协议可验安全性形式化分析. 中国工程科学, 2010,1(l2): 67-73.5 Kevin Benton. The Evolution of 802.11 Wireless Se
27、curity. INF795-April 18th,2010 UNLV Informatics Spring2010.6 R. Canetti and H. Krawczyk. Analysis of Key-Exchange Protocols and Their Use for Building Secure Channels. Advances in Cryptology-EUROCRYPT 2001,pp.453474,Springer-Verlag,2001.7 B LaMacchia, K Lauter and A Mityagin. Stronger Security of Au
28、thenticated Key Exchange. .8 Gast and S Matthe. 802.11 Wireless Networks: the Definitive Guide; creating &Administering Wireless Networks; Covers 802.11a, G, N & I. Beijing: OReilly,2007. Print.9 RFC 2865 - Remote Authentication Dial In User Service (RADIUS). IETF Web. .10 Finneran M F. Voice over W
29、LANs:The complete guideM. Boston:Elsevier,2008:280286.11 Fluhrer S, Mantin I and Shamir A. Weaknesses in The Key Schedule Algorithm of RC4C. The 8th Annual International Workshop on Selected Areas in Cryptography. London:Springer-Verlag ,2001:325.12 曹秀英,耿嘉,沈平. 无线局域网安全系统M. 北京:电子工业出版社,2006:153155.The
30、analysis and improvement on formal security models of three party authentication and key distributionAbstract：This paper analyses the formal security models of three party authentication and key distribution protocol,which are extended BR model and extended CK model. We present the flaw of three par
31、ty identity authentication in the extended BR model and suggest the limitation in the definition of matching conversation for extended CK model.According to the criterion flow of 802.11i, we make use of the conception of “efficiency AP” defines a new formal security model of three party authenticati
32、on and key distribution,and we present a EAP-TLS protocol and prove its security in our model. The new formal security model also provides method for resolving the security problem of three party authentication and key distribution in WLAN. Keywords: 802.11i; EAP protocol; Provable security; Three party formal security model
