基于OTP的移动商务身份认证协议设计与研究.doc

基于OTP的移动商务身份认证协议研究王秦国家自然科学基金资助项目：移动商务系统中的身份认证研究(60773033)作者简介：王秦，男，吉林省梨树县，1973年，北京交通大学博士研究生，移动商务身份认证，melonzn张润彤，男，辽宁省大连市，1963年，北京交通大学教授，信息安全、移动电子商务、网格计算等，rtzhang，张润彤(北京交通大学信息系统研究所，北京100044)摘要：安全问题已成为制约移动商务发展的瓶颈。身份认证是网络安全的第一道防线，安全、高效的移动商务身份认证协议是保证移动商务安全的必要条件。OTP认证技术实现简单、成本低、无须第三方认证的特点使其较适合移动商务的身份认证。椭圆曲线密码体制是现有公钥密码体制中运算效率、安全性最高且无须第三方的体制。本文基于OTP的认证思想，利用椭圆曲线密码体制实现数字签名和密钥协商，提出基于OTP的移动商务身份认证协议，设计其注册阶段、登陆阶段和同步重调阶段流程。形式化分析方法是分析认证协议存在安全漏洞的重要途径。串空间方法是现有认证协议形式化分析方法中最为直观、简洁、严格和有效的方法，利用串空间方法证明了基于OTP的移动商务身份认证协议的安全性。关键字：移动商务；身份认证；OTP；椭圆曲线密码；IMEI；串空间中图法分类号:TP393.04Research of Mobile Commerce Identity Authentication Protocol Based on OTPWang Qin, Zhang Run-tong(Institute of Information System, Beijing Jiaotong University, Beijing 100044, China)Abtract: The security has greatly limited development of mobile commerce. Identity authentication is the first defense line of network security, so a safety and effective identity authentication protocol is necessary to ensure mobile commerce. OTP(One-Time Password ) technology which is implemented simply, has low cost and needs no third authentication is more suitable for identity authentication in mobile commerce. Elliptic curve cryptography mechanism has the highest effectiveness and security, needs no third authentication among public-key cryptography mechanisms. Through improving the OTP technology, realizing signature and key agreement through elliptic curve cryptography mechanism, the identity authentication protocol is presented on basis of OTP, and its register, login and synchronous resetting procedure are designed. Formal analysis method is the main method to analyze security of authentication protocol and among them Strand Space method is simple, intuitive, strict and effective. The protocol is certificated to be secure through Strand Space method.Key words: Mobile commerce; identity authentication; OTP; Elliptic Curve Cryptography; IMEI; Strand Space1 引言在移动商务环境的安全机制中，身份认证处于核心地位，因为在缺乏对用户身份有效认证的前提下，用户信息的完整性和保密性没有任何意义可言1，因此，移动商务环境下身份认证的研究，对移动商务的安全体系，乃至对整个移动商务的推广与发展具有重大意义。2 移动商务的身份认证需求目前，移动商务的身份认证多基于GSM网络、短信息以及简单的用户静态口令认证，这些方法易受到攻击并且口令在无线传输中易被截获。非移动商务环境下的身份认证协议多采用基于公钥的认证体系，必须以完善的CA（Certification Authority，证书授权中心）体系为基础，需要一个合法的公正的第三方参与认证，这种方法成本高昂，技术复杂，不适合于目前尚不成熟的移动商务环境。移动商务通常以无线通信设备承载，而移动终端具有计算能力弱、存储空间小、电池供电量有限等特点，因此，移动商务身份认证协议必须具备运算负载低、内存使用量小和实现简单等特点。移动商务身份认证协议的设计需求主要为2-5：移动用户与移动网络的双向认证；移动用户与移动通信网络之间相互认证身份，这是在移动通信中被普遍认同的一个安全需求，也是安全通信中最基本的安全需求。但是在第二代移动通信系统中存在很多安全问题，其中之一就是缺少用户对移动网络的身份认证，导致“中间人攻击”的威胁。密钥协商和双向密钥控制；移动用户与移动通信网络之问通过安全参数协商确定会话密钥，保证一次一密。一方面可以防止由于一个旧的会话密钥泄漏而导致的重传攻击；另一方面可以防止由通信的一方指定一特定会话密钥带来的安全隐患，保证密钥质量。敏感数据（如移动用户身份信息）的机密性；有些用户为了防止自己的所在位置信息和行踪泄漏，需要对自己的身份信息进行保护，即身份信息不能以明文形式在网络传输。相关数据（如移动用户发送的数据）的不可否认即防止抵赖；移动通信中的某一方对自己发送或者接收到的某些数据在事后不能进行抵赖。这个特性对于部署移动商务不可缺少。认证协议尽量简单、计算量小、通信量小。考虑到目前移动通信系统的带宽受限，以及移动通信终端的计算资源有限，所设计的身份认证协议应保证尽量简单、计算量小、通信量小。即使在第三代移动通信系统中，带宽得到大幅度改善，目前硬件的瓶颈得到一定的突破，手持移动通信终端的体积和市场价格决定了其计算资源和存储资源的有限性。对于上述安全需求，并不是每种身份认证协议都要全部满足。在设计移动商务身份认证协议时，可根据具体情况需要，设计满足其中上述部分安全需求的移动商务身份认证协议。3 相关理论3.1 OTP实现机制及安全分析美国科学家Lamport6首次提出利用散列函数产生一次性口令的思想，即用户每次登录系统时使用的口令是变化的。一次性口令（One-Time Password，简称OTP），指用户在网上传送的口令只使用一次，从而使攻击者无法通过窃取用户口令非法访问系统。OTP技术的认证过程如图2-1：图3-1 OTP技术的认证过程OTP认证技术是一种比较简单的机制，它可以简单快速地加载到任何系统之上而无需附加硬件。选择OTP认证做为移动商务的身份认证机制，主要基于：OTP实现简单、无需十分复杂的算法，适合运算能力不高的移动终端；OTP由用户秘密的通行短语和挑战信息通过单向函数生成，具备一定的安全性；认证过程中客户端和服务器端通信次数不多，数据传输量小，适合目前移动商务网络速度尚不十分快速的情况；目前移动商务缺乏权威的第三方认证机构，相关法律也不健全，使用OTP认证无需第三方参与，避免了需第三方认证带来的诸多问题。OTP认证技术应用于移动商务身份认证具备一定的优势，但也存在一些问题：易遭受离线字典攻击7；攻击者可利用小数攻击获取一系列口令冒充合法移动用户8；仅支持服务器对客户端的单向认证，无法防范假冒的服务器欺骗客户端。OTP认证机制的安全隐患主要在于参与一次性口令生成的随机数以及口令认证信息都以明文方式传送，因此，如果采取密码体制对随机数及认证信息进行加密传输，必然给攻击者攻击行为带来巨大困难。3.2 椭圆曲线密码体制在目前的公钥密码体制中，椭圆曲线密码体制（Elliptic Curve Cryptography，ECC）以其安全性高、密钥长度短、加密和解密速度快等优点，成为当今密码学领域最有前途的密钥体制。所谓椭圆曲线指由韦尔斯特拉斯()方程9：+=+ 确定的平面曲线，其中系数(=1,2,6)定义在某个域上，可以是有理数域、实数域、复数域，还可以是有限域，椭圆曲线密码体制用到的椭圆曲线都定义在有限域上。椭圆曲线离散对数问题是构造椭圆曲线密码体制的数学基础。椭圆曲线离散对数问题（Elliptic Curve Discrete Logarithm Problem，简称ECDLP）定义如下10：给定素数和椭圆曲线，和是曲线上的点，对于=，在已知，的情况下求出小于的正整数。可以证明，已知和计算比较容易，而由和计算则比较困难，它比通常的离散对数问题更为难解，至今还没有有效的计算方法解决这个问题。ECC能比RSA等其它公钥加密系统提供更好的加密强度、更快的执行速度和更小的密钥长度，如160位密钥的ECC具有1024位密钥RSA及DSA相同的安全强度11，这使得密钥存储、内存使用及数字签名过程更为有效，同时ECC算法易于用软件硬件实现，因此最适合支持移动商务的安全需要。4 基于OTP的移动商务身份认证协议的设计4.1 设计思路基于OTP的移动商务身份认证协议设计思路如下：（1）使用移动设备特征性标识做为一次性因素的生成因子；（2）使用椭圆曲线加密算法产生客户端、服务器端的公钥和私钥，较传统的公钥算法效率更高；（3）利用哈希链构造一次性口令时加入服务计数，避免针对已知散列函数的小数攻击；（4）利用散列函数生成随机因子，避免了明文传输，而且替代了散列次数递减作为随机因子带来的哈希链长度不够问题；（5）认证口令传输时，客户端和服务器端分别用对方的公钥加密，在另一方用私钥解密，避免了明文传输，且对随机因子进行了二次加密，提高了口令传输的安全性。4.2 设计方案符号说明：参与认证的用户端：用来认证的服务器端：用户注册提供的用户身份标识：用户提供的口令，在注册时第一次提供，存储在客户端。以后每次认证，用户都需提供正确的用户密码：移动设备唯一标识（International Mobile Equipment Identity），也称为手机串号，作为客户端与服务器的认证口令因子而存在：哈希函数，为了叙述简便，以下使用代替|：运算符表示两端的信息或文字进行连接：服务器端生成的安全椭圆曲线密码系统的参数集：用户公钥：用户私钥：服务器公钥：服务器私钥：加密过程：解密过程：表示客户端第次登录：客户端接受服务的次数：客户端产生的一次性因素：服务器产生的一次性因素2.2.1 注册阶段设计注册阶段流程如下：（1）初始化生成安全椭圆曲线，选取自己的公钥和私钥；（2）向发起注册请求；（3）将椭圆曲线系统参数集连同发送给；（4）存储，并根据安全椭圆曲线系统选取自己的密钥对和；（5）输入和，并存储和，向发送利用加密的、以及，即；（6）接收，利用做运算，得到、和。验证是否已经存在其用户数据库中，如果存在，则向发送用户名重复的注册失败信息；（7）如果验证成功，则将与、绑定，并存入数据库。初始化为0，将与、绑定，生成一次性因素|并向发送注册成功信息，将做为认证阶段的随机因子被存储；（8）接收，将也初始化为0，将与绑定，生成一次性因素，存储在，注册阶段完成。注册阶段流程设计如图4-1：图4- 1 注册阶段流程设计2.2.2 登录（认证）阶段设计登陆阶段利用注册阶段产生的公钥和私钥对认证口令进行加密和解密。认证口令中的一次性因素是认证的关键因素，和计算和，通过比较验证双方的合法性。口令传输过程中，均用公钥进行加密处理。认证过程步骤如下：（1）输入和，计算，比较此计算值是否与移动设备存储的相同。若相同，继续；否则提示用户，口令错误；（2）向发起登录请求，产生，发送用加密后的、和，即，并保存；|)对于第一次登录的用户，|)；是一个关于初始的哈希链值，但并不是一次计算完全长度的哈希链，仅从上次认证的中迭代计算哈希值；（3）接收，利用做解密，即执行，得到、和。在数据库中查找和，若存在此用户，则根据查找保存在数据库中的，随后产生，发送利用用户的公钥加密的、，即，并保存；|)对于第一次验证：，|；（4）接收的信息后利用解密，即执行，得到和，并与刚才保存的比较，若相同，则通过对的验证，否则终止会话，认证结束。验证通过后，发送用加密后的，即；（5）接收，利用做解密，即执行，得到，并与刚才保存的比较，若相同，则通过对的验证，否则终止会话，认证结束。认证成功后，S将加1更新；（6）S发送成功信息给，也将加1更新。登录阶段（双向认证）流程设计如图4-2：图4-2 登录阶段流程设计2.2.3 同步重调设计正常登陆验证过程中双方计数器都会同步增1。但网络中存在各种各样的隐患和不可预测情况，会不可避免地出现这样或那样的情况。比如：成功通过验证，计数器增加1；但应答的数据包被黑客截获、篡改或丢失，这样就不能成功通过的验证，的计数器不会增加1。明显在这种情况下，和就会“失步”。同步重调设计流程如下：（1）将自己计数器值传送给；（2）将之与本身的计数器值进行比较，取较大的一个进行更新；（3）通知进行同样更新。  这个通信过程完成后，也就完成了“同步重调”工作。此时和的计数器值应该一样，且为之前两者中较大的一个。取两者中较大的一个，为了避免某两次使用同一个计数值计算出一样的一次性口令，保证一次性口令的唯一性。5 基于OTP的移动商务身份认证协议的串空间证明5.1 串空间的理论框架协议分析是揭示认证协议存在安全漏洞的重要途径。串空间方法是现有认证协议形式化分析方法中最为直观、简洁、严格和有效的方法12。本文利用串空间方法对基于OTP的移动商务身份协议进行认证性证明。5.1.1 基本术语主体：参与协议的各方，：参与协议运行的主体，：主体间的长期共享密钥，：主体的公开密钥，：主体的秘密密钥，：主体生成的临时值（通常是一次性随机数）：一般意义上的加密密钥，表示一个范围的概念：用加密密钥对数据进行加密，：数据和的连接：协议入侵者：入侵者初始知道的密钥集合5.1.2 串和串空间令集合中的元素为协议主体交换的消息，称的元素为消息项。消息项间最重要的关系是子项关系，记为，表示是的子项。（注：根据上下文，对于消息项，“”代表子项关系；对于集合，“”代表包含关系。）定义1 一个有符号项是一个二元组<,>，其中，是+号或-号。这样可以把一个有符号项记作+或-。()*表示有符号项的有限序列的集合，可以用<<,>, . <,>>表示集合()*的一个元素。定义迹为一个有符号项的有限序列。定义2 上的一个串空间是指一个串的集合，且在该集合上存在迹映射：:()*。通常用集合中的元素称为串。定义3 对于一个串空间：（1）结点是二元组<,>，其中，为满足1len(tr()的整数，称结点=<,>属于串或在串上，记作。显然，每一个结点都属于唯一的一条串。结点的集合用表示。（2）如果=<,>，用index()表示在的迹上的索引，那么index()=。定义项()为的迹上第个有符号项（表示在结点发送或接收的消息），相应地，用-项()表示的迹上第个有符号项的非符号部分。如果项()的符号是正的（或负的），称结点是正的（或负的）。（3）如果,，那么表示项()=+，项()=-。它表示结点发送消息，节点接收消息，记录了串间的一种因果连接。（4）如果,，那么表示,出现在同一条串上，且index()=index()-1；它表示是在串上的直接因果前驱。而表示是在同一个串上的因果前驱（不一定是直接因果前驱）。（5）无符号项出现在，当且仅当项()。（6）无符号项在结点生成，当且仅当项()的符号为正，项()，并且对于同一串上的任意前驱结点，有项()。（7）无符号项是唯一生成的，当且仅当唯一起源于。（8）无符号项不生成，当且仅当不存在使得在生成。由前面的定义可知，串空间构成一个有向图(,)，是结点集合，边=()。束是有向图(,)的一个子图，可以用图中的有向边和表示结点间的因果依赖关系。定义4 设是串空间中部分边的集合，是和中任意边相关联的结点的集合，是和的并集。是一个束，如果满足：（1）是有限的；（2）若，并且项()是负的，那么存在一个唯一的结点，使得 ；（3）若，且，那么且；（4）是无环的。5.2 基于串空间的认证测试方法认证测试方法是以串空间模型为基础的一种用于验证认证协议安全性的方法，它保留和使用了串空间模型中对于关于协议、状态和主体的基本定义和性质，通过构造测试分量，应用认证测试规则判断安全协议是否能够达到身份认证、信息保密等安全目标13。定义5 设是一个束，为一个串，,，则对于，若为负结点为正结点，则是转换边，若为正结点为负结点，则是被转换边，项()，并且产生一个新的分量，使得。定义6 是在上的测试分量，则（1），是的分量；（2）不是任何一个正常结点的子项，。如果唯一产生于结点，则是的测试，并且是的被转换边。定义7 若是对的测试，且，则它是在的出测试，其中仅包含在的分量中，是在中的测试分量。若是对的测试，且，则它是在的入测试，是在中的测试分量。若是任何在中的测试分量，且，则负结点是的一个主动测试。认证测试方法提出三种不同的认证测试，根据测试分量的类型选择相应的方法对协议能够满足的认证和保密属性进行证明，认证测试方法的使用能够简化协议分析的过程。对应于三种不同的测试类型，测试方法也分为三类12：认证测试1 设是一个束，是在的出测试，则（1）存在正常结点，使得是的分量，且是对于的变换边；（2）假设仅存在于的分量中，不是任何一个正常分量的真子集，且，则存在一个负的正常结点，为该结点的分量。认证测试2 设是一个束，是在的入测试，则存在正常结点，使得是分量，且是的转换边。认证测试3 设是一个束，是的一个主动测试，则存在一个正常结点，且是的一个分量。使用认证测试方法进行协议分析可以分为四个步骤14：（1）根据协议描述构造协议中所有主体的串；（2）按照协议的安全目标选择测试分量；（3）确定测试分量的类型，分为出测试、入测试和主动测试；根据测试分量的类型选择认证测试方法：出测试对应认证测试1；入测试对应认证测试2；主动测试对应认证测试3；（4）应用认证测试规则对测试分量中的内容进行验证，确定协议能够满足的安全目标，以及不能够得到证明的目标。5.3 认证阶段证明协议描述如下：（1）：（2）：（3）：（4）：成功消息按照串空间方法，协议第（4）步可省略，协议描述为（1）：（2）：（3）：其中，代表发起者，代表响应者，、为主体、产生的随机数，、分别为主体、的公钥，相应的、为主体、的私钥。从图中可以看到，串空间模型将协议的执行过程使用有向图表示，“”表示不同串之间的状态转换，“”表示同一个串中不同状态之间的转换。使用串空间模型分别建立起发起者串和响应者串。发起者串及其轨迹为：，响应者串及其轨迹为：，其中，,，,。前提假设为：,，并且,分别由、唯一产生。在串空间模型中协议的消息交换过程如图5-1： 图5-1 基于OTP的移动商务认证协议的串空间模型1. 身份认证发起者端的证明（证明服务器端的身份）（1）构造测试分量；由于唯一产生于结点，因此，是的测试分量，从上图可以得到构造了在的出测试。（2）应用认证测试；应用认证测试1得到存在正常结点，使得项()=，并且是的转换边。（3）定义结点；由第2步的结果可得为负结点。假设为某个响应者串中的结点，并且项()=。（4）比较串的内容；比较项()和响应者串中的相应分量，可以得到，。（5）证明；使用认证测试1的第二部分，将作为测试分量，且。因此，存在一个正常结点,为负，项()=。（6）定义结点；假设为某个发起者串中的结点，项()=且符号为负。（7）比较串和的内容；由于唯一产生于初始串，且，因此可以得到=。由于-=项()，最终可以得到。由此可得，发起者能够对响应者的身份和产生的随机数进行认证。响应者端的证明（证明客户端的身份）（1）构造测试分量；由于唯一产生于结点，因此，是的测试分量，从上图可以得到构造了的出测试。（2）应用认证测试；应用认证测试1存在正常结点，使得项()=，并且是的转换边。（3）定义结点；由第2步的结果可得为负结点，因此，为某个初始串中的结点，假设该初始串为，且，并且项()=。（4）比较串的内容；通过比较项()和发起者串中的内容可以得到，。由此可得，响应者能够对发起者的身份和产生的随机数进行认证。根据以上证明，主体和都能够向对方证明自己的身份，从而满足了安全协议设计的身份认证原则，有效避免了中间人攻击。2. 保密性证明和初始产生的随机数、能够满足保密性的设计原则。假设是该协议的束，发起者串，,，是安全的密钥集合。证明：设，为不安全的密钥集合，如果有一个结点，并且项()，则存在一个合法结点是的入口点()。但是协议合法主体和产生的所有消息项内容都以加密密文形式传输，并且，因此，、不会被攻击者截获，能够满足保密性的设计原则。3. 数据认证主体和在收到对方发送的消息后，分别要向对方发送确认信息以证明和正确接受了、。假设是该协议的束，发起者串和响应者串分别为：，。，,，。证明：由于在端唯一产生，如图5-3所示，协议的前两条消息构造成的出测试，为的转换边。通过前面身份认证的结果可以得到，。因此证明证明端确实正确的接受到，并发送确认信息到端，由此证明协议满足的数据认证原则。同端的证明过程相似，端通过协议的后两条消息构造的出测试，为的转换边。根据前面身份认证的证明结果得到，。因此，证明端正确接收到，并发送确认信息到端，由此证明协议满足的数据认证原则。综上，基于OTP的移动商务身份认证协议能够满足数据保密性、身份认证、数据认证的安全目标。由于现有的消息项内容已经能够满足安全协议的要求，因此，无需增加其它冗余信息。6 结论本文首先分析移动商务的身份认证需求，指出移动商务的身份认证协议应具备简单、计算量小、通信量小等特点。OTP认证技术是一种比较简单的认证机制，通过引入椭圆曲线密码体制对其进行改进，提出了基于OTP的移动商务身份认证协议，实现了双向认证，解决了OTP认证技术存在的安全隐患，并用串空间方法证明了其安全性。参考文献：1胡志远.口令破解与加密技术M.北京:机械工业出版社.20032G Horn, K M Martin, C J Mitchell. Authentication Protocols for Mobile Network Environment Value-Added ServicesJ. IEEE Transaction on Vehicular Technology. 2002,51(2):99-1003李晓瑾,童恒庆一次性口令认证技术的改进J.电脑开发与应用,2004,17(9):28-304贾红涛移动电子商务的安全性分析及其身份认证设计D.哈尔滨:哈尔滨工业大学,2005.6 5王洪莹.移动商务身份认证系统的研究与设计D.北京交通大学,2007.6 6Lamport L. Password authentieation with insecure communicationJ. Communication of the ACM, 1981,24(11):770-7727汤鹏志,李黎青,左黎明基于SHA的一次性口令认证技术J.华东交通大学学报,2005,22(2):55-598许正伟,程晓荣.基于改进OTP的用户身份认证技术的研究与实现J.微机发展,2004,14(6):109-1149N Kanayama,T Kobayashi,T Saito et al. Remarks on elliptic curve discrete logarithm problemJ, IEICE Trans Fundamentals,2000:1722.10肖脩安.椭圆曲线密码体系研究M.武汉:华中科技大学出版社,200611刘志猛,赵燕丽.无线网中基于ECC的认证和密钥交换协议J.燕山大学学报,2008,32(1):1-3,912王亚第,束妮娜,韩继红,王娜.密码协议形式化分析M.北京:机械工业出版社,200613李谢华基于串空间模型的安全协议形式化验证方法的研究D上海交通大学,2007,114陆超，周颖，陈波，赵保华基于串空间的Kao_Chow加密协议形式化验证J中国科学技术大学学报，2007,37(12):1529-1533