Simpl' protocol HLPSL specification

This file contains HLPSL specification of authenticated key-exchange protocol called Simpl' (based solely on cryptographic one-way hash functions), which is quantum computing resistant and suitable for IoT devices. The HLPSL file can be used with AVISPA formal verification tool.

本文件包含名为Simpl'的认证密钥交换协议的高级协议规范语言（High Level Protocol Specification Language, HLPSL）规范。该协议仅基于密码学单向哈希函数构建，具备抗量子计算特性，适用于物联网（Internet of Things, IoT）设备。HLPSL格式文件可配合AVISPA形式化验证工具使用。