An analysis of security protocols for lightweight systems
Date
2022-04
Journal Title
Journal ISSN
Volume Title
Publisher
Stellenbosch : Stellenbosch University
Abstract
ENGLISH SUMMARY: Security is hard to maintain in distributed systems especially for communicating
agents restricted to lightweight computations, as in the Internet of Things, which
struggle to implement strong cryptographic security. A methodology is developed
for specifying and reasoning algebraically about security in such systems which
combines epistemic logic and a state-based formalism. The knowledge modality
K is used to define a uthentication a nd s ecrecy i n t erms o f w hat e ach agent
knows. Operations are defined a s s tate t ransitions. Having g ained c onfidence in
our methodology by applying it to the benchmark case studies Needham-Schroeder
and Diffie-Hellman protocols, we then apply it to the contemporary examples Signal
and Long-Range Wide-Area Network protocols. A mitigation is proposed and
verified for a Long-Range Wide-Area Network.
AFRIKAANS OPSOMMING: Sekuriteit is moeilik om te handhaaf in verspreide stelsels, veral vir kommunikasieagente met beperkte berekenings vermoë, soos Internet van Dinge, wat sukkel om sterk kriptografiese s ekuriteit t e i mplimenteer. ‘n Metodologie word ontwikkel vir die spesifikasie e n a lgebraïes r edenering a angaande s ekuriteit v ir s ulke sisteme. Hierdie metodologie maak van epistemiese logika en ‘n staat gebaseerde formalisme gebruik. Die kennismodaliteit K word gebruik om verifikasie e n geheimhouding te definieer i n t erme van wat e lke a gent w eet. Operasies word a s staatsoorgange gedefinieer. Nadat vertroue in die metodologie verkry word deur dit op die maatstaf gevallestudies van die Needham-Schroeder- en Diffie-Hellman protokolle toe te pas, word dit vervolgens op die hedendaagse voorbeelde van Sein en Langafstand Wye-area netwerk protokolle toegepas. ‘n Versagting word vir ‘n Langafstand Wye-area netwerk voorgestel en geverifieer.
AFRIKAANS OPSOMMING: Sekuriteit is moeilik om te handhaaf in verspreide stelsels, veral vir kommunikasieagente met beperkte berekenings vermoë, soos Internet van Dinge, wat sukkel om sterk kriptografiese s ekuriteit t e i mplimenteer. ‘n Metodologie word ontwikkel vir die spesifikasie e n a lgebraïes r edenering a angaande s ekuriteit v ir s ulke sisteme. Hierdie metodologie maak van epistemiese logika en ‘n staat gebaseerde formalisme gebruik. Die kennismodaliteit K word gebruik om verifikasie e n geheimhouding te definieer i n t erme van wat e lke a gent w eet. Operasies word a s staatsoorgange gedefinieer. Nadat vertroue in die metodologie verkry word deur dit op die maatstaf gevallestudies van die Needham-Schroeder- en Diffie-Hellman protokolle toe te pas, word dit vervolgens op die hedendaagse voorbeelde van Sein en Langafstand Wye-area netwerk protokolle toegepas. ‘n Versagting word vir ‘n Langafstand Wye-area netwerk voorgestel en geverifieer.
Description
Thesis (PhD)--Stellenbosch University, 2022.
Keywords
Lightweight computations, Computer programming, Computer system security, UCTD