BAN邏輯介紹
BAN邏輯是一種基于知識和信任的形式邏輯分析方法，由Burrows，Abadi 和 Needham 提出，通過對認證協議的運行進行形式分析，從協議執行者最初的一些基本信仰出發，根據協議執行的每個參與者發出和收到的訊息，推理得到參與者的最終信仰，
BAN邏輯成功分析出NeedHam-Schroeder，Kerberos等協議的漏洞，
應用BAN邏輯對認證協議進行分析，首先需要進行理想化處理，將協議的訊息轉換成BAN邏輯中的公式，再根據具體情況進行合理假設，由邏輯的推理法則根據理想化協議和假設進行推理，推斷協議能否完成預期的目標，如果在協議流程結束時能夠建立關于共享通信密鑰、對方身份等的信任，則表明協議是安全的，
BAN邏輯運算式和推理規則
- BAN邏輯處理的物件：主體、密鑰和公式，
- BAN邏輯主要推理規則：訊息含義規則、亂數驗證規則、裁判規則和新鮮性規則等，
- BAN邏輯協議分析步驟：理想化步驟→確認初始假設→邏輯推理→得出結論，
運算式
推理規則
- 訊息含義規則
1.1 對于共享密鑰：
表示P相信K是P和Q之間的通信密鑰，當P看到用K加密的資訊X，則P相信Q曾經說過X，
1.2 對于公鑰：
表示P相信K是Q的公鑰，P看到用Q的私鑰加密的訊息，則P相信Q曾經說過X，
1.3 對于共享秘密：
- 亂數驗證規則：
表示P相信X是新鮮的，且P相信Q曾經說過X，則P相信Q相信X是真實的，
- 裁判規則：
表示P相信Q對X由控制權，且P相信Q相信X，則P相信X，
- 新鮮性規則：
如果P相信X是新鮮的，則P相信X和Y級聯的整體資訊也是新鮮的，
- 解密規則：
如果P看到用自己有效公鑰加密的資訊，則P可以解密看到資訊，
-
信仰規則：
-
發送規則：
如果P相信Q曾經發送過整個訊息，那么P相信Q曾經發送過訊息的子部分，
- 接收規則：
參考文獻
[1]于代榮,楊揚,馬炳先,劉明軍,王世賢.基于身份的TLS協議及其BAN邏輯分析[J].計算機工程,2011,37(01):142-144+148.
[2]張玉清,李繼紅,肖國鎮.密碼協議分析工具——BAN邏輯及其缺陷[J].西安電子科技大學學報,1999(03):116-118.
[3]投訓芳,郭金庚.用BAN邏輯方法分析SSL 3.0協議[J].計算機工程,2001(11):147-149.
未完待續……
轉載請註明出處，本文鏈接：https://www.uj5u.com/qita/555351.html
標籤：其他
上一篇：由淺入深了解機器學習和GPT原理
下一篇：返回列表