Kutatás vezetője: Németh L. Zoltán
Szervezet:
Leírás: Az Optin Sensor Protocol egy felhasználói adat-független kapcsolat-orientált kliens-szerver kommunikációs protokol. Az OSP 1.2 verziója nem tartalmazott kriptográfiai szolgáltatásokat. A projekt célja ezen protokol kriptográfia újratervezése volt, melyet mint OSP 2.0 publikáltunk. E cél elérése érdekében először fenygetés modellezést hajtottunk végre, masd összegyűjtöttük a biztosnági elvárásokat. Ezután megterveztünk az új változatot és elkészítettük annak referencia implementációját. Végül Tamarin-Proover automatikus tételbizonyító eszközt használtuk, mely segítségével a matematika pontosságával igazoltuk az új OSP 2.0 több fontos biztonsági tulajdonságát.
The Optin Sensor Protocol is a payload-agnostic connection-oriented Client-Server protocol with small overhead for use in IoT applications. The protocol contains specific features to solve problems that arise in these applications, like data transmission with minimal overhead, remote firmware updating, device control and configuration. The protocol also has features to eliminate transmission problems caused by unreliable over-the-air connections.
The 1.2 version of the protocol does not contain any security features, all data is transmitted as plain text, and neither the server, nor the client is authenticated beyond a simple plain text id/password pair.
The OSP 1.2 is already used in various applications including sensor data collection, telemetry, and medical applications. While most of the communication is performed on relatively secure channels like WiFi or GPRS, the need to provide security features at protocol level has arised with recent projects.
Most of the popular IoT protocols, MQTT for example, rely on lower layer security protocols like SSL and VPN, or optional payload encryption at application level, above the IoT protocol itself. Protocols that use asymmetric encryption methods require lots of computing power and memory, typically not available on devices that use OSP. To provide client and server authentication, payload encryption and integrity, we had to find a way to provide these features using symmetric cryptographic methods, preferably as an integral part of the protocol itself, while introducing as little overhead above OSP 1.2 as possible.
To start analysing edge case scenarios and possible attacks against the current protocol, we chose use-cases of the OSP with high security requirements and with high contrast between available lower layer services and computing power.
An example use case of the OSP where the device offers lots of computing power is a capnographic data streaming solution. A tabletop capnograph device measures the $\textrm{CO}_2$ concentration of exhaled air, while streaming measurement data to a server for further processing, storage, and display on a web interface. Given the transmitted data is sensitive medical information, confidentiality level is high, although no sensitive personal info (like name or other official ID) is transmitted. Data integrity and the authentication of both the client and the server are critical. The amount of data to be transmitted is relatively high, up to 0.5kB/s. The device connects to the cloud using a WiFi interface, while underlying services allow SSL/TLS to be used. As the device uses a wall adapter for power and contains a powerful single-board computer, there are no hard power or processing limits, allowing complex software-level cryptography, if needed.
The goal of this project was to do a security redesign of the protocol and publish a new 2.0 version of it. For this we first performed threat modelling, collecting several security expectations. Then, we provided the new design with a reference implementation. Finally, we used the Tamarin-Prover to prove some desired important security properties of the OSP 2.0 with mathematical correctness.
We published the new specification of the OSP version 2.0 on the website of our industrial partner: https://optin.hu/static/www/OSP_spec_v2_en.pdf
