Abstract: Data encryption and authentication based on public key system are not suitable for Wireless Sensor Network（WSN） because of the limitation of characteristic of nodes. SNEP protocol is an important part of SPINS protocol which features nodes very well. It is in charge of session key establishment and authentication between nodes based on trusted base station. This paper adopts CK model which is one of provable security model to construct a new protocol existed in ideal model corresponding to reality model, and then executes formal analysis by adversaries ADV and UDV which exist in two models respectively. The conclusion that SNEP protocol constitute security channel in reality environment has been obtained.

Key words: SNEP protocol, CK model, adversary, security channel

摘要： 无线传感器网络（WSN）由于受节点特点限制，不适合采用公钥体制进行数据加密以及身份认证等。SNEP协议是针对WSN特点提出的SPINS协议中的重要部分，主要负责基于可信基站的节点间会话密钥建立以及认证。采用可证明安全模型中的CK模型构建了一个理想模型下与现实模型下SNEP协议相对应的新协议，通过两种模型下的敌手ADV与UDV对它们进行形式化分析，得出SNEP协议构成了现实环境中安全通道的结论。

关键词: SNEP协议, CK模型, 敌手, 安全通道