Abstracts Category : Other

Formal verification and access control approach of an IoT protocol

by Douglas Simes Silva

Protocolos de Segurana esto na nossa rotina diria e exemplos distoso compras utilizando o carto de crdito, eleio eletrnica, redes sem fio e etc. O primeiro objetivo deste trabalho a verificao formal dos aspectos de segurana de um protocolo voltado para Wireless Sensor Networks (WSN). O Trustful Space-Time Protocol (TSTP) engloba a maioria das caractersticas necessrias para aplicaes WSN como por exemplo controle de acesso, roteamento geogrfico de pacotes, estimativa de localizao, relgio precisamente sincronizado, canais de comunicao segura e um esquema de distribuio de chaves entre o gateway e os sensores. Aps a anlise formal do protocolo de distribuio de chaves do TSTP usando Proverif, ns encontramos duas falhas de segurana: uma relacionada ao componente de sincronizao de tempo e outra relacionada ao mtodo mac-then-encrypt empregado. Com as falhas encontradas ns propmos uma verso melhorada do protocolo de distribuio de chaves. O segundo objetivo criar um esquema de controle de acesso sensvel ao contexto para dispositivos Internet de Coisas(IoC) usando TSTP como canal de comunicao. O esquema da poltica foi projetado para um cenrio Smart Campus e seu contexto. Aproveitamos os recursos do TSTP para adicionar dados de tempo e espao como contexto para o nosso modelo. Aps o desenho do modelo de poltica, descrevemos seu modelo simblico e fizemos uma anlise formal para ter certeza de que os valores das propriedades de contexto no 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.Advisors/Committee Members: Martina, Jean Everson (advisor), Moraes, Ricardo Alexandre Reinaldo de (advisor).