物联网（The Internet of Things,IoT）是IT产业中一项革命性技术,它通过将物理设备与互联网相连接的方式,为人们提供了统一的设备管理平台。其中,订阅式物联网系统基于发布/订阅通信模式,凭借优异的消息处理能力,成为了物联网系统的主流架构模式。在订阅式物联网系统中,设备负责收集环境中的数据并将其发布到互联网,用户则通过订阅系统提供的服务来获取所需的环境信息。随着订阅式物联网系统日益广泛的应用,其安全性和隐私性也引起人们的高度关注。基于信息中心网络的物联网系统（ICN-IoT）和强验证订阅式物联网系统（Au-thenticated Publish/Subscribe,AUPS）是两个旨在解决物联网安全性和隐私性问题的订阅式物联网架构,其中,ICN-IoT系统利用未来网络体系架构——信息中心网络（Information-Centric Networking,ICN）加强系统的安全性,ICN通过信息内容而非IP地址来标识网络对象,可以更好地支持面向数据本身的安全保护。AUPS系统则使用传统安全手段——访问控制技术来保障系统内重要数据的安全性,在AUPS系统中,用户只有在通过访问控制验证后才可以订阅物联网服务。作为加强系统安全性和隐私性的两种典型方案,ICN-IoT系统和AUPS系统受到的关注也日益增多,因此,针对两个系统安全性和隐私性的研究也变得至关重要。在本文中,我们使用形式化方法对以上两种订阅式物联网系统的安全性和隐私性进行研究。基于通信顺序进程（Communicating Sequential Processes,CSP）,我们建立ICN-IoT系统和AUPS系统的形式化模型。借助模型检测工具PAT（Process Analysis Toolkit）,我们抽象出两个模型在功能性、安全性和隐私性方面应该满足的性质,并对模型进行性质验证。验证结果表明,在引入入侵者的情况下,ICN-IoT系统和AUPS系统不能充分保障系统的安全性和隐私性。因此,我们分别对ICN-IoT系统和AUPS系统进行优化,然后借助PAT验证改进后的系统模型,根据验证结果,我们的工作可以加强两个订阅式物联网系统的安全性和隐私性。