通信網(wǎng)安全理論與技術(shù)課程第7講安全協(xié)議形式化分析與設(shè)計(編輯修改稿)
2025-02-13 11:18 本頁面
【文章內(nèi)容簡介】 見 X； P曾經(jīng)收到過包含 X的消息并且讀到 X P |~ X P曾經(jīng)說過 X； P曾經(jīng)發(fā)送過包含 X的消息 P |= X P可以裁定 X；相信 P對于 X的真值的判定 (X) X是新鮮的； X在當(dāng)前協(xié)議運行前沒有被發(fā)現(xiàn)過 P和 Q共享一個好的密鑰 k：“好”代表 k依舊具有保密性 P具有密鑰公鑰 k(私鑰是 k1)，這個私鑰只有 P以及他信任的人知道 P和 Q分享秘密 X：這個秘密只有 P、 Q以及他們信任的人知道 {X}K 用 k加密 X后的消息 XY X與消息 Y結(jié)合 kPQ???k P???XPQ?BAN邏輯： 推理規(guī)則 ? 消息含義規(guī)則 – 使主體推知其他主體發(fā)送過的消息 ——說明消息的出處 ? 共享秘鑰情況 ? 公鑰情況 ? 共享秘鑰情況 | , { }1:| |~PQPQkkP Q P P XMP Q X? ? ??? ??, { }PQ PQk kP b e li e v e s Q P P s e e s XP b e li e v e s Q s a id X? ???1| , { }2:| | ~kkP Q P XMP Q X?? ??? ??1, { }kkP b e l i e v e s Q P s e e s XP b e l i e v e s Q s a i d X????|,3:| |~XYP Q P P XMP Q X? ? ? ? ??,X YP b e lie v e s P Q P s e e s XP b e lie v e s Q s a id X? ?? ? ?BAN邏輯： 推理規(guī)則 ? 臨時值驗證規(guī)則 – 使主體推知其他主體的信仰 | ( ) , | |~1:||P X P Q XNP Q X????,P b e lie v e X is fr e s h P b e lie v e Q s a id XP b e lie v e Q b e lie v e XBAN邏輯： 推理規(guī)則 ? 管轄規(guī)則 – 拓展了主體的推知能力 ? 使主體可以在基于其他主體已有的信仰之上推知新的信仰 | | , | |1:|P Q X P Q XJPX? ? ? ??,P b e lie v e Q c o n tr o l X P b e lie v e Q b e lie v e XP b e lie v e XBAN邏輯： 推理規(guī)則 ? 接收消息規(guī)則 – 定義了主體在協(xié)議運行中對消息的獲取 ? 規(guī)則 1 ? 規(guī)則 2 ( , )1: P X YRPX??2: YPXR PX? ? ??( , )P sa w X YP sa w XYP sa w XP sa w X??BAN邏輯： 推理規(guī)則 ? 接收消息規(guī)則 – 定義了主體在協(xié)議運行中對消息的獲取 ? 規(guī)則 3 ? 規(guī)則 4 | , { }3: PQ PQk kP Q P P XRPX? ? ??? ??| , { }4: k kP P P XRPX? ??? ??, { }PQ PQk kP b e li e v e Q P P s a w XP s a w X? ???, { }k kP b e lie v e P P s a w XP s a w X???BAN邏輯： 推理規(guī)則 ? 接收消息規(guī)則 – 定義了主體在協(xié)議運行中對消息的獲取 ? 規(guī)則 5 1| , { }5: QkkP Q P XRPX?? ??? ??1, { } QkkP b e li e v e Q P s a w XP s a w X????BAN邏輯： 推理規(guī)則 ? 信仰規(guī)則 – 反映了信念在消息的級聯(lián)與分割的不同操作中的一致性 ? 規(guī)則 1 ? 規(guī)則 2 | , |1: | ( , )P X P YB P X Y???| ( , )2:|P X YBPX??,( , )P b e lie v e X P b e lie v e YP b e lie v e X Y( , )P b e lie v e X YP b e lie v e XBAN邏輯： 推理規(guī)則 ? 信仰規(guī)則 – 反映了信念在消息的級聯(lián)與分割的不同操作中的一致性 ? 規(guī)則 3 ? 規(guī)則 4 | | ( , )3: ||P Q X YB P Q X????| ~ ( , )4:|~P Q X YBP Q X??( , )P b e lie v e Q b e lie v e X YP b e lie v e Q b e lie v e X( , )P b e lie v e Q s a id X YP b e lie v e Q s a id XBAN邏輯： 推理規(guī)則
教學(xué)課件相關(guān)推薦
鄂ICP備17016276號-1