Formal verification and access control approach of an IoT protocol

Abstract

Protocolos de Segurança estão na nossa rotina diária e exemplos distosão compras utilizando o cartão de crédito, eleição eletrônica, redes sem fio e etc. O primeiro objetivo deste trabalho é a verificação formal dos aspectos de segurança de um protocolo voltado para Wireless Sensor Networks (WSN). O Trustful Space-Time Protocol (TSTP) engloba a maioria das características necessárias para aplicações WSN como por exemplo controle de acesso, roteamento geográfico de pacotes, estimativa de localização, relógio precisamente sincronizado, canais de comunicação segura e um esquema de distribuição de chaves entre o gateway e os sensores. Após a análise formal do protocolo de distribuição de chaves do TSTP usando Proverif, nós encontramos duas falhas de segurança: uma relacionada ao componente de sincronização de tempo e outra relacionada ao método mac-then-encrypt empregado. Com as falhas encontradas nós propómos uma versão melhorada do protocolo de distribuição de chaves. O segundo objetivo é criar um esquema de controle de acesso sensível ao contexto para dispositivos Internet de Coisas(IoC) usando TSTP como canal de comunicação. O esquema da política foi projetado para um cenário Smart Campus e seu contexto. Aproveitamos os recursos do TSTP para adicionar dados de tempo e espaço como contexto para o nosso modelo. Após o desenho do modelo de política, descrevemos seu modelo simbólico e fizemos uma análise formal para ter certeza de que os valores das propriedades de contexto não foram adulterados.

Abstract : Security protocols are included in our every day routine. A few examplesare credit card purchases, e-voting, wireless networks, etc. Thefirst goal of this dissertation is the formal verification of the securityaspects of a cross-layer, application-oriented communication protocolfor Wireless Sensor Networks (WSN). The Trustful Space-Time Protocol(TSTP) encompasses a majority of features recurrently needed byWSN applications like medium access control, geographic routing, locationestimation, precise time synchronization, secure communicationchannels and a key distribution scheme between sensors and the sink.After the security protocol analysis of TSTP?s key distribution protocolusing ProVerif we were able to find two security flaws: one related tothe time synchronization component and another being a bad approachrelated to a mac-then-encrypt method employed. With our findingswe propose an improved version of the key distribution protocol. Thesecond goal is to create a context-aware access control scheme for Internetof Things(IoT) devices using TSTP as a communication channel.The policy?s scheme was designed for a Smart Campus scenario andits context. We take advantage of TSTP?s features to add time andspace data as context for our model too. After the design of the policymodel, we described its symbolic model and we did a formal analysisto be sure that the context properties values were not tampered.