Security model and analysis of access delegation

Abstract

Organizing access control for example in shared rooms, workplaces, bikes, hotels and homes can sometimes be difficult and costly. One way to overcome the problems, for example in key delivery, is to have a mobile application that works as a virtual key. In this thesis, we study a commercial application that supports the following features. The user can request access to a lock for a certain time period on a website. Then the user can use the mobile application to access the lock offline using Bluetooth Low Energy (BLE) or Near-Field Communication (NFC). In addition, the user can delegate single accesses to third parties offline.

The aim of the thesis is to formally verify that the cryptographic protocol between the phone and the electronic lock is secure. That is, no unauthorized parties can access the lock even if they tamper with the messages that the phone and the lock exchange through the BLE/NFC channel. We verified the security of the protocol using Tamarin, a symbolic verification tool for cryptographic protocols.

During the course of the work, we found two weaknesses related to the time constraints of the delegation. We provided improvements to the protocol to counter these attacks and we verified the security of the improved protocol.

Jaetut huoneet, työpaikat, kaupunkipyörät, hotellit ja kodit vaativat kaikki jonkinlaista kulunvalvontaa. Tilanteesta riippuen kulunvalvonta voi olla haastavaa ja kallista järjestää. Eräs ratkaisu tähän on mobiilisovellus, joka toimii virtuaalisena avaimena. Tässä työssä tutkimme kaupallista sovellusta, joka mahdollistaa virtuaalisten avainten jakamisen ja käytön.

Sovelluksen käyttäjä voi tilata internetin kautta pääsyoikeuden lukkoon tietylle ajalle ja sen jälkeen avata lukon sovelluksella Bluetooth Low Energy (BLE) tai Near-Field Communication (NFC) kanavan yli ilman, että lukko tai käyttäjä ovat yhteydessä internettiin avaushetkellä. Lisäksi käyttäjä voi jakaa yksittäisiä avauskertoja muille ilman verkkoyhteyttä. Tätä kutsutaan käyttöoikeuksien delegoinniksi.

Tämän diplomityön tarkoituksena on varmentaa formaalisti, että mobiililaitteen ja lukon välillä käytetty kryptografinen protokolla on turvallinen. Toisin sanoen varmistamme, että vain halutut käyttäjät pystyvät avaamaan lukon, vaikka ulkopuolisilla tahoilla olisi mahdollisuus muokata Bluetooth LE ja NFC kanavan yli lähetettyjä viestejä.

Varmensimme protokollan turvallisuuden automaattisella Tamarin-työkalulla, joka on tarkoitettu kryptografisten protokollien symboliseen verifiointiin. Verifiointi paljasti protokollasta kaksi heikkoutta, jotka liittyivät delegoinnin aikarajoituksiin. Esittelemme tässä työssä korjausehdotukset, jotka poistavat heikkoudet. Lisäksi varmistimme Tamarinilla, että korjattu protokolla on turvallinen.