基于CSP物聯(lián)網(wǎng)通信協(xié)議的建模與形式化分析研究.pdf

1、針對(duì)物聯(lián)網(wǎng)通信協(xié)議安全性不足和使用非形式化方法對(duì)協(xié)議的安全性進(jìn)行分析時(shí)容易出現(xiàn)錯(cuò)誤的問題,通過分析物聯(lián)網(wǎng)感知層協(xié)議中的Hash-lock協(xié)議、隨機(jī)Hash-lock協(xié)議、David數(shù)字圖書館協(xié)議,發(fā)現(xiàn)這些協(xié)議存在閱讀器非法掃描標(biāo)簽和協(xié)議主體沒有會(huì)話密鑰的安全隱患問題。為了解決這兩個(gè)安全問題研究了增強(qiáng)物聯(lián)網(wǎng)通信協(xié)議安全性方法,該方法使用了適合此特征的異或運(yùn)算和具有單向性質(zhì)的哈希函數(shù)進(jìn)行加密處理,采用形式化的分析方法對(duì)其安全性進(jìn)行分析驗(yàn)證。

2、
　　物聯(lián)網(wǎng)感知層設(shè)備有計(jì)算能力有限、存儲(chǔ)能力有限和供電能力有限的特點(diǎn),DDL2P通信協(xié)議使用了適合此特征的異或運(yùn)算和具有單向性質(zhì)的哈希函數(shù)進(jìn)行加密處理。在DDL2P協(xié)議運(yùn)行之前,除了在服務(wù)器中注冊(cè)標(biāo)簽的ID和共享密鑰外,增加了注冊(cè)標(biāo)簽閱讀器的ID值和共享的密鑰k,在協(xié)議中增加了對(duì)Tag閱讀器進(jìn)行認(rèn)證;同時(shí)對(duì)新鮮值進(jìn)行加密傳送;服務(wù)器在它們進(jìn)行認(rèn)證的同時(shí),產(chǎn)生一個(gè)會(huì)話密鑰并通過加密方式傳送給Tag閱讀器和Tag標(biāo)簽,這樣在后續(xù)的通

3、信中便可以使用會(huì)話密鑰進(jìn)行加密傳送。解決了Hash-lock協(xié)議、隨機(jī)Hash-lock協(xié)議、David數(shù)字圖書館協(xié)議沒有對(duì)讀寫器進(jìn)行認(rèn)證,以及以明文方式傳送消息的安全缺陷,由此解決了讀寫器非法掃描和信息安全傳送的問題。
　　對(duì)通信順序進(jìn)程CSP形式化分析理論進(jìn)行了研究。研究了CSP的數(shù)理基礎(chǔ)進(jìn)程代數(shù)、跡的概念、相關(guān)的定理和符號(hào)。對(duì)設(shè)計(jì)的協(xié)議,先使用CSP理論對(duì)協(xié)議進(jìn)行分析建模,然后把其轉(zhuǎn)化成一個(gè)CSP系統(tǒng),把協(xié)議主體建模成CSP