文档介绍：年 月
第 34 卷 第 3 期 计 算 机 工 程 2008 2tn)由时间戳(Ta或Tb)联接随机字节(Ra或Rb)而成。
KUb
A相信Kab是他和主体B之间的秘密密钥； A|≡ B ，A相信 Mccv中的握手消息为
KUb是B的公开密钥；A|≡B|⇒C，A相信B是命题C的权威。使 Mhs=Ta,Ra,Tb,Rb,CA,B,Tkb,KUb, {H(CA,B,Tkb,KUb)}KRCA,P,G,Kb,
用GNY逻辑分析密码协议：(1)确定协议的初始状态假设；(2) {H(P,G,Kb,Ta,Na,Tb,Nb)}KRb,CA,A,Tka,KUa, {H(CA,A,Tka, K
利用协议解析器将协议步骤翻译成逻辑描述；(3)根据初始假 Ua)}KRCA,Ka
H(T ,N ,T ,N ,P,G,K )=MD5(T ,R ,T ,R ,P,G,K )+SHA-1(T ,R , T ,
设、协议的逻辑描述和推理规则进行推理，得出各方持有的 a a b b b a a b b b a a b
Rb,P,G,Kb)
最终拥有集和信念集。本文指出了GNY逻辑的主要命题和协
H(Mhs)=MD5(Mhs)+SHA-1(Mhs)
议分析过程[1-2]，分析了EAP-TLS[3-5]密码协议。
完成消息为
1 EAP-TLS 认证和密钥交换协议消息的描述 MF=H(Kms,H(Mhs))=PRF(Kms,〝FL〞, MD5(Mhs)+ SHA-1 (Mhs))
EAP-TLS 认证机制的无线客户端和服务器先申请一个 客户完成消息为
标准的