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

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

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

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