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.