随着无线网络技术的迅速发展,民用飞机机载信息域在机场环境下,使用Gatelink与机场Wi Fi连接,实现与机场及航空公司专网的通信。为保证“飞机-地面”连接的安全性,实现民用飞机机载信息域与航空公司网络设施间的安全通信,Gatelink引入了可扩展认证协议。可扩展认证协议(EAP)是一种广泛使用的身份验证框架,提供了多种认证子协议,在为Gatelink提供安全认证服务的同时,也面临诸多安全威胁。本文重点研究EAP-TLS扩展认证方法,以改进当前EAP-TLS认证方案的安全性为基本出发点,对现有主流的EAP-TLS认证方案存在的安全问题进行分析,提出了一种EAP-TLS认证协议改进方案,并对其安全性进行了分析和自动化证明。具体研究内容如下:分析Shojaie Bahareh等人和Jingjing Zhang等人提出的EAP认证方法,发现现有EAP-TLS认证方法存在三个安全缺陷。第一,在未经认证的情况下,服务器以明文方式发送自身公钥,攻击者在客户端和服务器之间实时监听,可以直接获得并篡改服务器公钥,在通信双方毫不知情的情况下,完成认证,实现中间人攻击;第二,认证过程中客户端使用未经认证的密钥加密自己的身份,攻击者可直接获取客户端身份并对身份进行篡改,导致认证过程失败,或者直接泄露用户身份;第三,客户端和接入点之间以明文的方式发送EAP-Success报文,攻击者截获Success响应包并篡改为Logoff,致使客户端主动断开与认证系统的连接并重新发起认证,重复多次,导致服务器认证次数到达上限并关闭认证端口,停止向客户端提供服务,实现Do S攻击。针对以上安全问题,本文提出一种改进的EAP-TLS认证协议方案,该方案第二阶段采用ECDSA签名机制,客户端和服务器分别对证书和随机数进行签名,客户端、接入点和服务器分别解密签名,进行相互认证,保证认证实体的合法性,有效抵御中间人攻击;第二阶段,服务器使用ECDSA签名机制对自身证书进行签名,客户端验证服务器证书合法性,使用验证合法的服务器公钥对自己的身份进行RSA非对称加密,并将绑定的身份与证书一同发送给认证方,有效防止身份攻击;第三阶段服务器使用AES对称加密机制对EAP-Success进行加密,防止攻击者直接截获EAP-Success响应包,有效抵御Do S攻击。本文对EAP-TLS认证协议改进方案的安全性进行工具辅助的自动化分析。采用形式化分析工具ProVerif,使用Applied PI演算建立各种密码原语并描述安全协议。针对各安全属性,向安全协议描述中插入相应的质询语句,获得自动化属性验证的结果。证明结果显示,本文提出的改进认证协议具备相互认证、密钥的安全性、消息的完整性、抵抗中间人攻击、抵抗Do S攻击、抵抗身份攻击等安全属性,同时,本文还从理论上分析了该协议具备的抵抗重放攻击、抵抗冒名攻击、前向保密性等安全属性。通过与Shojaie Bahareh等人和Jingjing Zhang等人提出的EAP认证协议进行安全属性对比分析,自动证明了Shojaie Bahareh等人的协议不满足抵抗中间人攻击、抵抗Do S攻击、抵抗身份攻击属性,Jingjing Zhang等人的协议不满足抵抗Do S攻击属性,证明了本文协议改进的有效性。本文还分析了各协议的通信开销和计算开销,表明提出的方案的实用性。