UCAP：云計算中一種PCL安全的用戶認證協議

李學峰，張俊偉，馬建峰

?

UCAP：云計算中一種PCL安全的用戶認證協議

李學峰1,2，張俊偉2，馬建峰2

（1. 青海廣播電視大學教育信息技術與資源建設中心，青海 西寧 810008；2. 西安電子科技大學計算機學院，陜西 西安 710071）

云計算利用網絡使IT服務變得彈性可變，如果用戶需要登錄到云端來使用服務與應用，系統需要確保使用者的身份合法，才能為其服務。為此，提出一種面向云計算協議組合邏輯（PCL, protocol composition logic）安全的用戶認證協議（UCAP）。UCAP引入了可信第三方，使用基于對稱加密密鑰的認證方法，確保參與認證雙方的相互認證，實現協議會話的認證性和密鑰機密性。協議主要分成2個階段：初始認證階段，由可信第三方生成根會話密鑰后，認證雙方相互認證；重認證階段，不需要可信第三方的參與，認證雙方快速生成子會話密鑰并實現相互認證。在協議組合邏輯模型下給出所提協議的形式化描述并利用順序組合證明方法分析了所提協議的安全屬性。同其他相關協議比較及實驗分析表明，UCAP在不影響安全性的前提下，提高了用戶認證的通信與計算效率，不但在重認證階段不依賴可信第三方，而且整個過程不依賴可信第三方同步時鐘。

云計算；用戶認證；協議組合邏輯；機密性；相互認證

1 引言

基于互聯網技術的云計算模型被視為下一代IT技術，它以資源租用、應用托管、服務外包為核心，迅速成為計算機技術發展的熱點[1]。云計算的開放性和復雜性決定了其安全性面臨著比傳統信息系統更為嚴峻的挑戰[2-3]。作為安全需求的第一道防線，身份認證也面臨著新的挑戰與威脅，這就需要一個有效的身份認證協議。

面對云計算安全威脅，需要采用加強身份認證機制，即相互認證等多種辦法，來保護云計算環境下的用戶數據。

云安全聯盟（CSA, cloud security alliance）在《云計算安全指南（3.0）》中提出了身份認證即服務的概念，它包括云服務中的身份、權限及授權或訪問管理中任何一部分的管理工作，身份認證即服務也是安全即服務的一項重要內容。當用戶試圖訪問云計算服務時，借助身份提供商（IdP, identity provider）的協助，完成與云服務提供商（CSP, cloud service provider）的認證。因此，通過可信第三方（TTP, trusted third party）協助用戶與CSP相互認證，對CSP來說降低了安全成本，對用戶來說能夠明確他們所獲得的安全服務，同時使CSP遵守清晰、一致的服務標準。

基于密碼技術的認證協議從協議設計的角度可分為無信任管理中心和有信任管理中心這2類。在無信任管理中心認證協議中，一般有基于口令[4-5]、基于用戶生物特征[6]、基于雙方持有秘密[7]的認證協議；在有信任管理中心的認證協議中，一般可以分為基于對稱密鑰的認證協議[8-9]和基于非對稱密鑰的認證協議[10-11]。通過分析可知，上述協議雖然存在一些不足，但采用有信任管理中心基于對稱加密的身份認證機制是一個可取的辦法。

使用TTP協助通信雙方相互認證，為避免重放攻擊，一般要求通信雙方與TTP時鐘保持同步，但在分布式云環境下，由于變化的和不可預見的網絡時延的特性，很難做到較好的時鐘同步。因此，需要避免時鐘同步的缺陷。

當用戶與CSP完成認證后，為了保證雙方會話的安全性，協議應能快速更新會話密鑰。為減少運行開銷且更好地適用云環境公開通信的應用需求，更新會話密鑰時不需要TTP的參與。

另外，在云計算環境下所設計的協議需要保證其在獨立計算情況下是安全的，在網絡環境下的運行也是安全的?；谶壿嫷膮f議組合（PCL, protocol composition logic）[12]模型是形式化證明協議安全屬性正確性的一種有效方法。目前，PCL已經用于證明基于Differ-Hellman的密鑰交換和簽名的STS協議族[12]（如IKEv2協議等）、Needham-Schroeder協議族[13]（如Kerberos V5協議[14]）以及WLAN安全標準[15]（如IEEE802.11i協議[16]和4G無線安全接入方案[17]）等。

根據上述云計算身份認證和協議安全性的需求，本文提出的用戶身份認證協議具有以下特點：1) 滿足協議組合安全；2) 基于對稱加密的相互認證；3) 可信第三方協助認證；4) 不依賴時鐘同步；5) 支持快速密鑰更新，更新時不涉及TTP。

2 相關工作及PCL模型

2.1 相關工作

近年來，許多學者針對云環境下身份認證的問題做了大量工作。文獻[8-9]基于對稱密碼體制，解決了用戶認證問題，但該協議依賴時鐘同步，如果TTP或票據服務器任何一個服務終止，用戶將無法繼續認證，且用戶身份認證的計算開銷和通信開銷較大。文獻[18]采用基于公鑰的密碼體制解決了用戶與CSP之間的身份認證問題，但公鑰證書的管理和維護會消耗巨大的計算資源。文獻[19]面向云存儲提出基于口令的三方認證密鑰交換協議，解決了數據接收方和數據發送方的認證，但由于采用的混沌映射系統復雜性高，序列性質不易控制。文獻[20-21]面向云計算數據存儲提出了基于橢圓曲線的認證機制，與RSA方案相比，該機制有效降低了計算成本。文獻[22-23]面向云計算提出了基于分層身份管理的認證思想，解決了證書管理問題。文獻[24]面向云計算提出了基于身份的用戶認證協議，雖然加強了用戶的安全屬性，但認證過程仍需指數運算。

上述文獻不能完全滿足前述云計算環境下身份認證協議的特點。因此，本文基于身份認證即服務的思想提出一種基于對稱加密的、由可信第三方協助的、支持快速密鑰更新的、可組合的身份認證協議（UCAP）。該協議包含初始認證和重認證這2個階段。初始認證階段：TTP分發相互認證實體的根會話密鑰；重認證階段：不需要TTP的參與，快速生成子會話密鑰。本文給出了UCAP的系統模型和方案描述，在PCL模型下描述了協議Cord演算、前提條件、不變量，并使用順序組合證明方法證明了協議的認證性和機密性。最后與其他文獻方案進行比較，結果顯示：與文獻[17,19]相比，UCAP不依賴同步時鐘；與文獻[17,19,21,24]相比，UCAP具有較高的計算效率、通信效率，且能快速生成子會話密鑰。

2.2 PCL系統

PCL是一種支持協議屬性證明的Floyd-Hoare類型的邏輯推導模型，它由Cord演算、協議邏輯（包括語法和語義邏輯）、證明系統組成[12,14]。

協議組合邏輯是邏輯地證明網絡協議的安全屬性，使用Cord來描述協議行為。PCL提供了組合證明方法（compositional proof method）和抽象改進方法（abstraction and refinement methodology）這2類可組合安全證明方法[12]。本文使用的術語、行為和串等相關語法、PCL邏輯語法、協議動作公理可參考文獻[12]。

2.3 PCL組合證明方法

安全證明包含個體行為，保證屬性的局部論證和忠實的遵循協議誠實主體的全局論證。多數協議證明使用式[]，它表示從狀態為真的狀態開始，在線程執行動作之后，也為真。協議組合邏輯PCL采用標準邏輯概念，提出認證屬性是協議動作之間的時間匹配關系，只推理誠實主體的動作即可證明攻擊下協議的安全性，并通過邏輯公理和模塊化推理方法支持復雜安全協議的組合推理，可以用來證明安全協議的認證性和機密性等安全屬性。順序組合證明方法的主要思想是：首先分析子協議的安全性，并將前一步的證明分解為2個部分，一部分使用誠信準則（honest rule）證明協議的不變量，另一部分不使用honest rule，將不變量作為假設證明協議；接著在更弱的前提下，協議的安全屬性應該能夠得到保證；然后應用順序規則，將二者進行順序組合；最后證明組合后的不變量對2個子協議都成立。由此可以得出，子協議的安全性在順序組合下得到保證。

3 系統模型及安全目標

3.1 系統模型

本文方案的協議模型如圖1所示，模型主要由用戶、云服務提供商和可信第三方組成。

圖1 本文方案的協議模型

1) 用戶（User）：用戶需要與云服務提供商進行數據交換或需要云服務提供商提供服務，可能是一個用戶或一個企業。在獲取會話密鑰后，經過安全傳輸，用戶可以訪問服務提供商提供的相關服務。

2) 云服務提供商（CSP）：CSP負責提供云解決方案，在與用戶協商會話密鑰后，與用戶建立會話，并提供相關服務。

3) 可信第三方（TTP）：TTP是一個可信實體，它總是行為誠實的，并將得到用戶和云服務提供商的信任，即它按照協議規范做出反應，而不會參與任何破壞其他主體安全的活動，在TTP的幫助下，用戶和云服務提供商這2個主體之間即便完全不認識，也可以實現相互認證和安全傳輸。TTP主要負責生成參與主體的會話密鑰。

本文引入的TTP從密碼學協議設計角度上看，是邏輯存在的，在現實部署中，TTP可以租用，也可以由CSP自身維護，本文所指TTP在其他文獻中可能稱為PKG（private key generator）、KGC（key generate center）或KDC（key distribution center）。

3.2 敵手模型

1) TTP是可信的，并且不會泄露密鑰，也不會泄露與其他用戶間的共享長期密鑰。

2) 信道被敵手控制，整個網絡通信環境是不可信的，敵手可以對數據流進行修改或偽造。

3) 假設敵手不能攻破底層的密碼算法而獲取相關密鑰。

4) 假設敵手不能攻陷TTP。

3.3 安全目標

總體來說，本文有以下安全目標：1) 確保長期共享密鑰和會話密鑰的機密性和認證性；2) 確保會話密鑰的機密性；3) 確保會話密鑰的時限性。

用戶、CSP預先與TTP安裝了長期共享密鑰，在初始認證階段有以下安全目標。

1) 用戶、CSP與TTP進行身份認證以確保其認證性。

2) TTP生成并分發根會話密鑰，會話密鑰具有機密性，即會話密鑰除TTP外僅由用戶、CSP共享。

3) 會話密鑰具有機密性。

在重認證階段有以下安全目標。

1) 用戶與CSP進行相互認證以確保認證性。

2) CSP驗證確保密鑰時限性。

3) 用戶與CSP更新子會話密鑰。

4) 確保更新后的會話密鑰具有機密性。

4 方案描述

UCAP涉及3個主體：用戶、CSP、TTP，分別用來表示，其中，分別和共享長期會話密鑰E、E。在云計算環境中，與進行安全傳輸時，必須要通過的許可才可以進行下一個動作，在本協議模型中，和為參與者，他們與分別共享長期密鑰K、K，并約定一種對稱加密機制，E(·)表示使用密鑰執行對稱加密操作。這時，需要參與云計算的每一方在注冊并與共享長期會話密鑰。

本協議可分為2個階段，初始認證階段（密鑰生成、認證階段）和重認證階段。具體描述如下。

4.1 初始認證階段

假設和與的長期共享密鑰由進行管理，并且使用統一的對稱加密算法，例如AES或DES等。

1)將自己的標識和加密信息發送給預期接收的對象，此時的加密信息是將用戶產生的隨機數R以及和的標識用與的長期共享密鑰E進行加密。

2)把從接收到的加密信息連同自己產生的時間戳T的標識、會話密鑰有效期限和共享的長期共享密鑰進行加密，再將加密結果和的標識、的標識以及產生的隨機數一起發送給可信第三方機構。

(2)

3)在接收到來自的消息后解密，然后生成2個消息并保留產生的隨機數R，第一個消息由的標識、與間的會話密鑰的隨機數R、的時間戳T以及會話密鑰有效期限組成，用和的長期共享密鑰（E）對所有第一個消息進行加密；第二個消息由的標識、與間的會話密鑰、的時間戳T以及會話密鑰有效期組成，用和的長期共享密鑰對所有第二個消息進行加密，然后將這2個消息連同的隨機數一起發送給。

4)解密第一個消息，提取與間的會話密鑰，并確認R的值是否與1)中的值一樣。發送2個消息給，第一個消息是從接收到的用E加密的消息，第二個消息是用與間的會話密鑰加密的的隨機數R。

5) 隨后，用它的密鑰解密消息，提取與間的會話密鑰密鑰有效期，并確認R的值是否與2)中的值一致。

如果時間戳和隨機數都匹配，和就會相信對方的身份，并共享一個會話密鑰。協議中的時間戳僅相對于的時間，所以不需要同步時鐘，只需要檢查自己產生的時間戳即可。

4.2 重認證階段

假設和完成了上述的協議，然后終止連接，如需重認證則不必依賴，且能夠在3步之內重認證。

1)將在4.1節的3)中發給它的“票據密鑰”和一個新的隨機數與的標識發送給云服務提供商。

重認證過程可以多次重復，直到過期為止，另外，新的隨機數也防止了重放攻擊。

5 基于PCL的協議安全性分析

5.1 UCAP形式化描述

分別以角色執行動作Cord的描述，如表1所示。

5.2 前提條件、安全屬性和不變量

5.2.1 前提條件

UCAP方案包括這3個主體，且與分別有共享會話密鑰和，UCAP的2個階段的前提條件如表2所示。

5.2.2 安全屬性

UCAP中用來分配與間的會話密鑰及會話票據，其安全屬性包括認證性和機密性。UCAP的2個階段的安全屬性如表3所示。

5.2.3 不變量

在UCAP中，利用PCL中的誠實準則，基于角色的協議動作順序以及與的會話密鑰的不變量描述如表4所示。

表1 A、B、S角色執行動作Cord的描述

表2 UCAP的前提條件

表3 UCAP安全屬性

表4 UCAP的不變量

5.3 安全性證明

在UCAP第一階段、第二階段中，根據的Cord演算、前提條件、不變量，分別基于的角色進行安全性證明，由于篇幅限制，本節只給出基于角色的證明過程，詳細證明過程參見附錄I和附錄II，基于角色的證明過程類似于角色的證明過程。

由于篇幅限制，定理1和定理2的證明過程見附錄I和附錄II。

定理3和定理4的證明過程與定理1和定理2的證明過程類似。

5.4 組合安全性

UCAP由1和2的協議順序組合而成，UCAP的證明使用PCL中順序組合的安全性證明方法。

證明 協議順序組合的安全性證明如下。

證畢。

其他參與方的證明過程與的證明過程類似，通過證明可以得出，UCAP方案在第一階段和第二階段具有相應的安全屬性，順序組成形成UCAP整體方案時也具有相應的安全屬性。接下來，通過定性與定量相結合的方法來對相關協議進行比較。

表6 協議性能比較

6 相關協議比較

為了有效地說明新協議UCAP的性能優勢，從理論和實驗這2個層面對上述協議參與方進行了對比分析，分別如表5~表7和圖2所示。為統一比較，將文獻中所提協議進行命名，其中，文獻[8]記為Kerberos，文獻[19]記為3PAKE，文獻[21]記為EPP，文獻[24]記為IDP。

表5從協議功能上對本文所提UCAP與其他相關協議進行了總結，具體符號含義如下。

F1：TTP參與。

F2：依賴時鐘同步。

F3：快速生成會話密鑰，更新時不涉及TTP。

F4：基于對稱的認證機制。

F5：相互認證。

F6：密鑰建立。

F7：已知會話密鑰安全性。

F8：抵抗重放攻擊。

表5 協議功能及安全性比較

表6從協議性能上對本文所提UCAP與其他相關協議進行了總結，其中，C為混沌映射操作、H為Hash操作、E/D為對稱加/解密操作、Ep/Dp為公鑰加/解密操作、Ec為橢圓曲線密鑰交換算法、G為概率生成操作、R為確定性復制操作、M為模運算，IC為初始認證、RC為重認證，CN為通信輪次。

表7從協議計算時延上將UCAP和其他相關協議進行了對比。實驗時，在單機上測試協議計算、認證時延，而不考慮發送消息時的傳輸時延。本機硬件環境為：CPU為i5，內存為4 GB；軟件環境為：系統為Windows7；測試語言為C++。

表7 協議計算時延對比（單位為ms）

圖2在不同CPU主頻下對Kerberos、3PAKE、UCAP的認證時延進行了比較。

圖2 不同CPU主頻下的認證時延

從表5~表7和圖2可以看出，與當前主流的用戶認證協議相比，在完成相同任務的情況下，新協議UCAP的應用場景、通信效率和計算效率具有優勢，具體分析如下。

1) 應用場景

如表5所示，所比較協議均需要TTP參與，3PAKE和Kerberos協議需要和TTP同步時鐘。在快速生成會話密鑰時不需要TTP參與，只有UCAP可以實現，符合云環境下公開通信的應用要求。

2) 通信效率

如表6所示，在IC階段的通信輪次上，UCAP最少，3PAKE、EPP、Kerberos協議居中，IDP最高。從總體上看計算開銷，UCAP最低，Kerberos協議次之，EPP和IDP較高。從用戶角度看，UCAP計算開銷最低，Kerberos協議次之，IDP最高。從TTP角度看，UCAP與3PAKE協議計算開銷相當，TTP最高。從CSP角度看，Kerberos協議計算開銷最低，UCAP次之。從用戶、CSP、TTP這3個角色看，根據云計算的特點，CSP應承載更多的計算開銷，用戶次之，TTP最少。除IDP、Kerberos協議外，其余協議均能滿足上述特點。在RC階段，除UCAP外，其余協議均需要TTP參與來完成密鑰更新。UCAP在密鑰更新過程中，僅需3輪通信即可完成密鑰更新，在通信效率上，與其他協議相比也具有較為明顯的優勢。

3) 計算效率

如表7所示，新協議的計算負載要明顯低于其他協議，UCAP較Kerberos協議在用戶、CSP、TTP端的計算時延分別下降了57.65%、9.04%和66.67%，較3PAKE協議在用戶、CSP、TTP端的計算時延分別下降了34.32%、27.54%、35.79%。新協議UCAP各參與方的整體計算時延較Kerberos、3PAKE、EPP、IDP協議降低了51.41%、32.48%、83.94%、71.60%。由于協議EPP、IDP的計算時延較長，圖2僅對Kerberos、3PAKE、UCAP各參與方的整體認證時延進行了比較。從圖2可以看出，隨著CPU主頻的提高，3個協議的認證時延整體下降，但新協議UCAP具有更低的認證時延。因此，基于對稱密鑰算法在實現通信雙方相互認證的基礎上，提高了認證雙方的計算效率。

4) 安全性分析

綜上所述，新協議UCAP在不失安全性的前提下，在應用場景、通信效率與計算效率方面性能優勢明顯。

7 結束語

在云計算環境中，安全問題是一項極具挑戰的問題[25]。針對參與云計算用戶認證的安全問題，本文在研究認證協議的基礎上，面向云環境提出了一種安全的用戶認證協議。該協議基于TTP分發根會話密鑰、CSP分發生成子會話密鑰的思想，使用對稱密鑰算法將協議方案分為2個階段，第一階段通過TTP實現用戶認證及根會話密鑰的分發，第二階段不涉及TTP實現用戶認證及子會話密鑰的生成，并且2個階段均不依賴TTP同步時鐘。在PCL模型下對UCAP進行協議組合證明，證明結果表明，所提協議在PCL模型下具有密鑰機密性和會話認證性。最后通過相關協議比較的結果表明：UCAP在不失安全性的前提下，降低了通信雙方的計算開銷，提高了通信效率，并且不依賴TTP同步時鐘，子會話密鑰的生成及用戶重認證不需要TTP的參與，符合云環境下公開通信的需求。因此，在云計算環境中本文所提方案具有一定的應用價值。

附錄I

定理1證明過程如下。

AN3,AA2,AP1(8) 式(8),,AF3(9) 式(8),,AF3(10) 式(8),AA1,P1(11) DEC,REC(12) 式(9)~式(11),AF1,ARP(13) 式(9),式(10),式(13),CP3(14) 式(14),PROJ,DEC,CP3(15) (16) ГUCAP(17) 式(12)~式(16)(18) 式(13),式(18),G1-3(19) 式(13),式(19),AF2(20) 式(8),式(9),AF2(21) (22) (23) 式(18),式(23),CP3(24) 式(24)(25) 式(25),(26) AA1,P1(27) 式(26),式(27),CP3(28) DEC,PROJ,(29) (30) (31) 式(31),(32) 式(13),式(19)~式(24),式(32)(33)

證畢。

附錄II

定理2證明過程如下。

P3(34) (35) ,AF2(36) 式(34)~式(36), AF1,ARP(37) (38) (39) 式(37)~式(39), Computes(40) 式(40)(41)

證畢。

定理3和定理4的證明過程類似于定理1和定理2。

[1] 林闖, 蘇文博, 孟坤, 等. 云計算安全: 架構, 機制與模型評價[J]. 計算機學報, 2013, 36(9): 1765-1784.

LIN C, SU W B, MENG K, et al.Cloud computing security: architecture , mechanism and modeling[J]. Chinese Journal of Computers, 2013, 36(9): 1765-1784.

[2] KANDUKURI B R, RAKSHIT A. Cloud security issues[C]//IEEE International Conference on Services Computing. 2009: 517-520.

[3] XIAO Z, XIAO Y. Security and privacy in cloud computing[J]. IEEE Communications Surveys & Tutorials, 2013, 15(2): 843-859.

[4] BOYKO V, MACKENZIE P, PATEL S. Provably secure password-authenticated key exchange using Diffie-Hellman[C]// International Conference on the Theory and Applications of Cryptographic Techniques. 2000: 156-171.

[5] MACKENZIE P, PATEL S, SWAMINATHAN R. Password-authenticated key exchange based on RSA[C]//International Conference on the Theory and Application of Cryptology and Information Security. 2000: 599-613.

[6] BERTINO E, PACI F, FERRINI R, et al. Privacy-preserving digital identity management for cloud computing[J]. Bulletin of the Technical Committee on Data Engineering, 2009, 32(1): 21-27.

[7] BRAINARD J, JUELES A, KALISKI B S, et al. A new two-server approach for authentication with short secret[C]//The 12th Conference USENIX Security. 2003: 201-214.

[8] KOHL J, NEUMAN C. The Kerberos network authentication service (v5)[R]. 1993.

[9] HOJABRI M. Innovation in cloud computing: implementation of Kerberos version5 in cloud computing in order to enhance the security issues[C]//2013 International Conference on Information Communication and Embedded Systems (ICICES). 2013: 452-456.

[10] ZISSIS D, LEKKAS D. Addressing cloud computing security issues[J]. Future Generation Computer Systems, 2012, 28(3): 583-592.

[11] BINU S, MISBAHUDDIN M, RAJ P. A mobile based remote user authentication scheme without verifier table for cloud based services[C]//The Third International Symposium on Women in Computing and Informatics. 2015: 502-509.

[12] DATTA A. Security analysis of network protocols: compositional reasoning and complexity-theoretic foundations[D]. Stanford University, 2005.

[13] ZHNG J, MA J F, YANG C. Protocol derivation system for the needham-schroeder family[J]. Security and Communication Networks, 2015, 8(16): 2687-2703.

[14] DATTA A, DEREK A, MITCHELL J C, et al. Protocol composition logic (PCL)[J]. Electronic Notes in Theoretical Computer Science, 2007, 172: 311-358.

[15] ZHANG H, CHEN L. An efficient authentication protocol of WLAN and its security proof[C]//The 2008 International Conference on Communications and Networking. 2008: 1133-1137.

[16] HE C, SUNDARARAJAN M, DATTA A, et al. A modular correctness proof of IEEE 802.11i and TLS[C]//The 12th ACM conference on Computer and communications security. 2005: 2-15.

[17] 王麗麗, 馮濤, 馬建峰. 協議組合邏輯安全的4G無線網絡接入認證方案[J]. 通信學報, 2012, 33(4): 77-84.

WANG L L, FENG T, MA J F. Secure access authentication scheme for 4G wireless network based on PCL[J]. Journal on Communications, 2012, 33(4): 77-84.

[18] URIEN P, MARIE E, KIENNERT C. An innovative solution for cloud computing authentication: grids of EAP-TLS smart cards[C]//2010 Fifth International Conference on Digital Telecommunications (ICDT). 2010: 22-27.

[19] LI C T, LEE C W, SHEN J J.A secure three-party authenticated keyexchange protocol based on extended chaotic maps in cloud storage service[C]//The 2015 International Conference on Information Networking (ICOIN). 2015: 31-36.

[20] ZISSIS D, LEKKAS D. Addressing cloud computing security issues[J]. Future Generation Computer Systems, 2012, 28(3): 583-592.

[21] YIN X C, LIU Z G, LEE H J. An efficient and secured data storage scheme in cloud computing using ECC-based PKI[C]//2014 16th International Conference on Advanced Communication Technology(ICACT). 2014: 523-527.

[22] YAN L, RONG C, ZHAO G. Strengthen cloud computing security with federal identity management using hierarchical identity-based cryptography[C]//IEEE International Conference on Cloud Computing. 2009: 167-177.

[23] GOEL A, GUPTA G, BHUSHAN M, et al. Identity management in hybrid cloud[C]//2015 International Conference on Green Computing and Internet of Things (ICGCIoT). 2015: 1096-1100.

[24] YANG J H, LIN P Y. An ID-based user authentication scheme for cloud computing[C]// 2014 Tenth International Conference on Intelligent Information Hiding and Multimedia Signal (IIH-MSP). 2014: 98-101.

[25] QIAN L, LUO Z, DU Y, et al. Cloud computing: an overview[M]//Springer Berlin Heidelberg, 2009: 626-631.

UCAP: a PCL secure user authentication protocol in cloud computing

LI Xuefeng1,2, ZHANG Junwei2, MA Jianfeng2

1. Education Information Technology and Resource Construction Center, Qinghai Radio & Television University, Xining 810008, China 2. School of Computer Science & Technology, Xidian University, Xi’an 710071, China

As the combine of cloud computing and Internet breeds many flexible IT services, cloud computing becomes more and more significant. In cloud computing, a user should be authenticated by a trusted third party or a certification authority before using cloud applications and services. Based on this, a protocol composition logic (PCL) secure user authentication protocol named UCAP for cloud computing was proposed. The protocol used a symmetric encryption symmetric encryption based on a trusted third party to achieve the authentication and confidentiality of the protocol session, which comprised the initial authentication phase and the re-authentication phase. In the initial authentication phase, the trusted third party generated a root communication session key. In the re-authentication phase, communication users negotiated a sub session key without the trusted third party. To verify the security properties of the protocol, a sequential compositional proof method was used under the protocol composition logic model. Compared with certain related works, the proposed protocol satisfies the PCL security. The performance of the initial authentication phase in the proposed scheme is slightly better than that of the existing schemes, while the performance of the re-authentication phase is better than that of other protocols due to the absence of the trusted third party. Through the analysis results, the proposed protocol is suitable for the mutual authentication in cloud computing.

cloud computing, user authentication, protocol composition logic, confidentiality, mutual authentication

TP309

A

10.11959/j.issn.1000?436x.2018147

李學峰（1975?），男，安徽宿州人，青海廣播電視大學副教授，“西部之光”訪問學者（在西安電子科技大學訪學），主要研究方向為密碼學、協議設計與形式化分析等。

張俊偉（1982?），男，陜西西安人，博士，西安電子科技大學副教授，主要研究方向為密碼學、網絡安全等。

馬建峰（1963?），男，陜西西安人，博士，西安電子科技大學教授、博士生導師，主要研究方向為信息安全、密碼學與無線網絡安全等。

2017?07?05；

2018?07?01

張俊偉，jwzhangxd@126.com

國家自然科學基金資助項目（No.61472310, No.61372075）；國家高技術研究發展計劃（“863計劃”）基金資助項目（No.2015AA016007）；青海社會科學規劃課題基金資助項目（No.16034）

The National Natural Science Foundation of China (No.61472310, No.61372075), The National High Technology Research and Development Program of China (863 Program) (No.2015AA016007), The Social Science Planning Project of Qinghai (No.16034)