Security of Low Level IoT Protocols

摘要

Application of formal methods in security is demonstrated. Formalism for description of security properties of low level IoT protocols is proposed. It is based on security property called infinite step opacity. We prove some of its basic properties as well as we show its relation to other security notions. Finally, complexity issues of verification and security enforcement are discussed. As a working formalism timed process algebra is used.