物联网（Internet of Things,IoT）将包括传感器设备在内的多种节点连接起来,为用户提供了便捷的信息服务。然而物联网的高速发展也带来了诸多的安全挑战,身份认证（Authentication）则是解决物联网中安全问题的关键技术之一。在物联网身份认证的研究中,针对不同应用场景的身份认证方案被研究者提出。Ticket-Based物联网身份认证方案通过对传感器设备和外部网络用户的移动设备的双向认证,解决了外网用户对传感器设备数据的访问因安全考量而受限制的问题。这个具有各种新特点的方案有效填补了物联网身份认证研究中的空白,但目前尚未有研究对该方案进行形式化验证与分析。因此,从形式化方法的角度来研究该方案的安全性和可靠性有着重要的意义。本文使用形式化方法中的通信顺序进程（Communicating Sequential Processes,CSP）对该方案进行了建模与分析。我们将方案中的实体抽象为进程,详细刻画实体进程的行为以及通信交互过程,同时在模型中引入入侵者来模拟网络攻击行为,完成了对方案的整体形式化建模。考虑到现实物联网中存在的诸多安全威胁可能造成密钥泄露,我们也针对方案所使用的密钥遭受入侵者窃取的情况构建了形式化模型。然后,我们使用模型检测工具Process Analysis Toolkit（PAT）实现了所建立的模型,并验证了方案需要满足的四大性质:无死锁性、数据可得性、数据安全性以及数据真实性。通过性质验证,我们发现该方案在密钥泄露的情况下不能满足数据安全性与数据真实性。我们详细分析了验证结果,给出了导致这两个安全性质不满足的入侵者攻击方式。最后,为了增强该方案的安全性,我们对方案提出了两次符合实际的改进。第一次改进主要使用了Nonce技术,并借助了公开密钥加密技术。第二次改进则主要基于Previous Nonce技术。验证结果显示,第一次改进后的方案可以确保数据安全性,第二次改进后的方案可以同时保证数据安全性和数据真实性。结果表明我们的改进方法可以有效地提升该方案的安全性,使方案能够更加可靠地应用于实际的物联网场景中。