[發(fā)明專利]一種SM4密碼算法的形式化驗(yàn)證方法及系統(tǒng)

有效

• 申請?zhí)枺?/td>: 202110465793.4
• 申請日: 2021-04-28
• 公開（公告）號: CN112989395B
• 公開（公告）日: 2022-05-17
• 發(fā)明（設(shè)計(jì)）人: 陳振婭;楊明;吳曉明;楊美紅;丁青艷;穆超;王鑫;王彪;王繼志
• 申請（專利權(quán)）人: 山東省計(jì)算中心（國家超級計(jì)算濟(jì)南中心）
• 主分類號: G06F21/60
• 分類號: G06F21/60;G06F21/46
• 代理公司: 北京集佳知識產(chǎn)權(quán)代理有限公司 11227
• 代理人: 楊威

本申請公開了一種SM4密碼算法的形式化驗(yàn)證方法，所述方法包括：將SM4密碼算法的算法參數(shù)定義為安全整數(shù)類型；其中，所述算法參數(shù)包括明文輸入、加密結(jié)果、密文輸入、解密結(jié)果、主密鑰、密鑰常數(shù)、輪密鑰和s盒參數(shù)；確定基于F*框架的算法模塊的初始堆，并在所述初始堆的目標(biāo)緩沖區(qū)中添加所述算法參數(shù)；利用所述算法參數(shù)對所述SM4密碼算法的輪密鑰生成模塊、加密模塊和解密模塊進(jìn)行形式化驗(yàn)證，得到所述SM4密碼算法的形式化驗(yàn)證結(jié)果。本申請能夠在SM4密碼算法實(shí)現(xiàn)過程中保證內(nèi)存安全、避免受到時間側(cè)信道攻擊。本申請還公開了一種SM4密碼算法的形式化驗(yàn)證系統(tǒng)，具有以上有益效果。

技術(shù)領(lǐng)域

本申請涉及網(wǎng)絡(luò)與信息安全服務(wù)領(lǐng)域，特別涉及一種SM4密碼算法的形式化驗(yàn)證方法及系統(tǒng)。

背景技術(shù)

隨著互聯(lián)網(wǎng)技術(shù)的迅猛發(fā)展，計(jì)算機(jī)網(wǎng)絡(luò)技術(shù)被廣泛應(yīng)用于各行各業(yè)，網(wǎng)絡(luò)安全問題日益受到關(guān)注。網(wǎng)絡(luò)安全的基礎(chǔ)是安全協(xié)議，安全協(xié)議的實(shí)現(xiàn)依賴于密碼技術(shù)，用于通信中的密碼分發(fā)和身份認(rèn)證，以此保證網(wǎng)絡(luò)通信安全。但是，在密碼算法的常規(guī)實(shí)現(xiàn)中存在內(nèi)存安全和側(cè)信道攻擊的問題。

因此，如何在SM4密碼算法實(shí)現(xiàn)過程中保證內(nèi)存安全、避免受到時間側(cè)信道攻擊是本領(lǐng)域技術(shù)人員目前需要解決的技術(shù)問題。

發(fā)明內(nèi)容

本申請的目的是提供一種SM4密碼算法的形式化驗(yàn)證方法及系統(tǒng)，能夠在SM4密碼算法實(shí)現(xiàn)過程中保證內(nèi)存安全、避免受到時間側(cè)信道攻擊。

為解決上述技術(shù)問題，本申請?zhí)峁┮环NSM4密碼算法的形式化驗(yàn)證方法，包括：

將SM4密碼算法的算法參數(shù)定義為安全整數(shù)類型；其中，所述算法參數(shù)包括明文輸入、加密結(jié)果、密文輸入、解密結(jié)果、主密鑰、密鑰常數(shù)、輪密鑰和s盒參數(shù)；

確定基于F*框架的算法模塊的初始堆，并在所述初始堆的目標(biāo)緩沖區(qū)中添加所述算法參數(shù)；

利用所述算法參數(shù)對所述SM4密碼算法的輪密鑰生成模塊、加密模塊和解密模塊進(jìn)行形式化驗(yàn)證，得到所述SM4密碼算法的形式化驗(yàn)證結(jié)果。

可選的，利用所述算法參數(shù)對所述SM4密碼算法的輪密鑰生成模塊進(jìn)行形式化驗(yàn)證，包括：

調(diào)用所述輪密鑰生成模塊，并將計(jì)數(shù)器的當(dāng)前值加1；

判斷所述計(jì)數(shù)器的當(dāng)前值是否小于第一預(yù)設(shè)值；若是，則將所述主密鑰與第一常數(shù)的異或結(jié)果賦值給中間數(shù)據(jù)；若否，則對每組所述中間數(shù)據(jù)的最后三個結(jié)果與第二常數(shù)的異或結(jié)果執(zhí)行所述SM4密碼算法的非線性變換和線性變換得到第一運(yùn)算結(jié)果，將所述第一運(yùn)算結(jié)果與每組中間數(shù)據(jù)的第一個結(jié)果進(jìn)行異或運(yùn)算得到運(yùn)算結(jié)果并將所述運(yùn)算結(jié)果賦值給輪密鑰；

判斷所述計(jì)數(shù)器的當(dāng)前值是否小于第二預(yù)設(shè)值；若是，則進(jìn)入調(diào)用所述輪密鑰生成模塊，并將計(jì)數(shù)器的當(dāng)前值加1的步驟；若否，則輸出最近一次確定的輪密鑰；其中，所述第二預(yù)設(shè)值大于所述第一預(yù)設(shè)值；

若所述輪密鑰生成模塊對應(yīng)的后置條件被滿足，則判定所述SM4密碼算法的輪密鑰形式化驗(yàn)證已通過。

可選的，利用所述算法參數(shù)對所述SM4密碼算法的加密模塊進(jìn)行形式化驗(yàn)證，包括：

判斷計(jì)數(shù)器的當(dāng)前值是否小于第三預(yù)設(shè)值；若是，則對每一組加密中間值的最后三個結(jié)果和所述輪密鑰的異或結(jié)果執(zhí)行所述SM4密碼算法的非線性變換和線性變換得到第二運(yùn)算結(jié)果，將所述第二運(yùn)算結(jié)果和每組所述加密中間值的第一個結(jié)果進(jìn)行異或運(yùn)算得到新的加密中間值，將計(jì)數(shù)器的當(dāng)前值加1；若否，則進(jìn)入將所述加密模塊最后一輪加密生成的加密中間值進(jìn)行倒序變換得到加密結(jié)果的步驟；其中，所述加密中間值為所述加密模塊的每一輪加密結(jié)果；

若所述加密模塊對應(yīng)的后置條件被滿足，則判定所述SM4密碼算法的加密模塊形式化驗(yàn)證已通過。

可選的，利用所述算法參數(shù)對所述SM4密碼算法的解密模塊進(jìn)行形式化驗(yàn)證，包括：