网络安全协议的形式化分析与验证 作者 李建华 第六章 Internet密钥交换协议.pptVIP

6.4.2 IKE v2协议分析 首先分析采用预共享秘密认证的初始交换协议。 1．协议抽象 在HDR中含有两个重要的信息：SPI（安全参数索引，用于识别IKE-SA）和Message 1D（消息标识）。在协议抽象中省略SPI，假设双方都工作在正确的IKE-SA内（如果SPI被篡改，只能造成无法通信，或数据完整性检查失败，但不会影响安全性），保留Message ID，记为M（IKE v2规定请求和响应是一一对应的，它们有相同的Message 1D）。 6.4.2 IKE v2协议分析 在第1条消息中，发起者I提供了多个安全联盟供响应者R选择，我们统一将SAil、SArl记为SA1，即假设双方事先约定了一个安全联盟，这样，证明了I和R的SA1的一致性，也就证明了SArl SAil。入侵者可以篡改SAil，但是不能认证SAil；同理，SAi2和SAr2也统一记为SA2。 6.4.2 IKE v2协议分析 对预共享秘密认证，秘密通常是口令p。IKE v2要求将p扩展成强密钥，若用HMAC函数实现prf，则KIR=Hp（密钥填充）。可以省略KIR的计算过程，只假设KIR是双方预共享的密钥。因此，AUTH1和AUTH2的内容分别如下： AUTH1=H (M,SA1,gi,Ni,Nr,HSK-ai(I)) AUTH2= H (M,SA1,gr,Nr,Ni, HSK-ar(R)) 6.4.2 IKE v2协议分析 可选载荷和数据的完整性保护，可得到如下的初始交换密钥分配和认证协议： 6.4.2 IKE v2协议分析 2．协议的秘密性 定义6.9 在IKE v2协议里，设Bf型入侵串轨迹是-x,+gx， KP BP= 。 定义6.10 设（Σ,P）是IKE v2协议里包含入侵者串的串空间，P是全体入侵者串， 6.4.2 IKE v2协议分析 定义Σinit是全体发起者串集合，Σresp是全体响应者串集合。 6.4.2 IKE v2协议分析 命题6.7 协议双方共享一致的SK-d | SK-ai | SK-ar | SK-ei | SK-er等价于它们共享一致的i和r。 引理6.1 gx是诚实函数。 6.4.2 IKE v2协议分析 命题6.8 设C是（Σ,P）上的丛，I、 R T，i、r BP， sinit Init[M,SA1,i,r,Ni,Nr,I,R,SA2,TSi, TSr]在C上的丛高是4， sresp Resp[M, SA1, i, r, Ni, Nr, I, R, SA2, TSi, TSr]在C上的丛高是4，S={i,r}，k= K \S，则IK[S]是诚实的。 6.4.2 IKE v2协议分析 命题6.9 设C是（Σ,P）上的丛，SK-ei、SK-er KP，sinit Σinit在C上的丛高是4，sresp Σresp在C上的丛高是4，设S={SK-ei,SK-er,I,R}，k= K \{ SK-ei,SK-er}，则IK[S]是诚实的。 6.4.2 IKE v2协议分析 3．协议的认证性 命题6.10 设C是（Σ,P）上的丛，Kxy、SK-ex KP，则形如H (g)、{g}SK-ex的项不起源于C中的入侵节点。 6.4.2 IKE v2协议分析 命题6.11：设 (g)起源于常规串s， 如果s Σinit，则g=M,SA1,gi,Nx,Ny, HSK-ax(X)； 如果s Σresp，则g=M,SA1,gr,Ny, Nx, HSK-ay(Y)，其中，X、Y Tname。 6.4.2 IKE v2协议分析 命题6.12 设s是常规串，如果 (M,SA1,gi,Ni,Nr,HSK-ai(I))起源于s, I R，则 s Init[M,SA1,i,r,Ni,Nr,I,R,SA2,TSi,TSr]，Ni起源于s，该项起源于s,3。 如果 (M,SA1,gr,Nr,Ni,HSK-ar(R))起源于s，I R，则 s Resp[M,SA1,i,r,Ni,Nr,I,R,SA2, TSi,TSr]，Nr起源于s，该项起源于s,4。 6.4.2 IKE v2协议分析 命题6.13 设C是（Σ,P）上的丛，I R，Kir、SK-ei KP，Ni唯一起源于C中的节点。如果 s Init[M,SA1,i,r,Ni,Nr,I,R,SA2,TSi,TSr] 在C上的丛高是4，则存在常规串 sresp Resp[M,SA1,i,r,Ni,Nr