信息时代高效率快节奏的工作使人们忽视那些看似与正常系统运行关系不大其实贯彻全局的安全工作，终于使得安全工作的匮乏到达了引爆点。近年来的有线网安全事件呈指数级上升，使得专家学者们对无线网的安全性进行未雨绸缪的分析和研讨。作为无线网中的重要应用之一的无线传感器网络（WSN）因其在军事，工业，农业中的广泛应用和远大前景，其安全性更加值得研究方案和提出解决方法。不同于有线网，WSN节点间的物理信道是空气介质，而且节点通常部署在无人维护、不可控制的环境中。因此WSN的安全如何很大程度上由其安全协议决定。虽然在该领域已有先驱提出一些实用的协议，但这些协议对于应用不同的WSN局限性比较大、漏洞较多。安全协议的分析与设计已成为一项兼具创新性和挑战性研究课题。随着学术的深究和应用的进展，作为协议形式化分析中的翘楚可证明安全理论有效地应用于各种协议的分析和研究中。本文合适地将可证明安全理论中的CK模型引入WSN的安全协议SPINS的分析和论证。本文首先阐述了WSN的网络特性与安全需求，并在此基础上对SPINS协议的安全性进行初步的探讨。随后引入可证明安全理论并对其进行简单介绍，后文重点研究了CK模型的核心部分，并分析了其论证过程和证明方法。通过将CK模型中的理想模型和现实模型应用在SPINS协议中，将构建一个理想模型下与现实模型下SPINS协议相对应的新协议，分别在两种模型下对应的敌手ADV与UDV对它们进行形式化分析研究，通过各种攻击手段得出其安全性漏洞以及其满足的语义和多项式安全，最终推导出SPINS协议构成了现实环境中的安全通道的结论。