物联网技术在各行各业应用越来越广泛,对物联网技术的研究也越来越多。随着物联网技术中硬件和软件的广泛应用,安全问题也日益突出。对消息传递中的通信主体进行身份验证,对传输的数据进行保密,是物联网技术发展中安全要求的重要部分。形式化的分析和验证方法是通过形式化的语言进行安全协议的建模,根据前面的假设进行验证分析协议的安全性。形式化的分析方法是当前安全协议研究的重要方法。越来越多的形式化分析方法被提出,来验证协议是否存在安全隐患。本文首先阐述了物联网的概念及安全协议的基础知识,针对安全协议的形式化分析方法进行了假设、分析和验证。主要工作有:第一,对物联网概念和物联网安全协议进行了综述,分析了形式化分析法的分类和基础。第二,对基于串空间模型理论的形式化验证方法进行了分析,并通过对N-S协议进行分析,发现其中存在的安全漏洞,并对其进行了改进。第三,利用串空间模型理论,在安全协议的设计过程中很好的进行了指导。对设计出的安全协议进行了验证和分析,证明了协议的安全性。