This thesis analyzes Application Layer security protocols for certificate enrollment and management. EDHOC, Ephemeral Diffie-HellmanOver COSE, is a recently developed key exchange protocol whichis designed to provide authentication and key-exchange functionality with compact message sizes and minimum round-trip-time. The workof this thesis extends the EDHOC protocol with a certificate enrollment functionality, targeting IoT constrained devices and it has been implemented for analysis and evaluation purposes. The main scope of this document is to study the security, performance and scalability (in descendingorder of importance) of enrollment over EDHOC compared to other certificate enrollment protocols. / Detta examensarbete analyserar säkerhetsprotokoll av typen ApplicationLayer för certifikatregistrering och hantering. EDHOC, Ephemeral Diffie-Hellman Over COSE, har implementerats, analyserats och utvärderats. EDHOC är ett nyligen utvecklat Application Layer-protokoll som är utformat för att tillhandahålla autentiserings- och nyckelfunktionsfunktioner med kompakta meddelandestorlekar och minimala rundturstider, inriktat på IoT-begränsade enheter. Huvudområdet för examensarbetet är att studera säkerhet, prestanda och skalbarhet (i fallande ordning av betydelse) hos EDHOC jämfört med andra föreslagna Application Layer-säkerhetsprotokoll som utför certifikatsskrivning.

As the number of Internet of Things devices is increasing rapidly, it is of utmost significance that the implementations of protocols for constrained devices are bug-free. In general implementations of network protocols are error-prone due to their complex nature and ambiguities in the protocol specification. Implementations of network protocols often contain critical errors which could be exploited. To avoid bugs and vulnerabilities, the implementation of network protocols has to adhere to their specifications. The objective of this thesis is to use symbolic execution to test one implementation of the Ephemeral Diffie-Hellman Over COSE (EDHOC) protocol and one implementation of the Constrained Application Protocol (CoAP) against their specifications. The goal is to identify bugs such as crashes, non-conformances, memory errors, and security vulnerabilities that may occur if the implementations are not adhering to their specifications. The methodology to do this consists of three steps: 1) extracting requirements from the protocols Request For Comments and expressing them as formulas, 2) preparing the system under test for symbolic execution and applying the formulas during symbolic execution to detect any paths that violate a requirement, 3) for every path which violates a requirement, the concrete value that the symbolic execution engine provided is used in the unmodified implementation to validate the bug. In total seven non-conformances were found which have been reported to developers. One non-conformance was found in the EDHOC implementation and six were found in the CoAP implementation. / Eftersom antalet Internet of Things enheter ökar snabbt är det av yttersta vikt att imple-menteringarna av nätverksprotokoll för Internet of Things enheter är korrekta. Generellt sett är implementeringar av nätverksprotokoll felbenägna på grund av deras komplexa natur och oklarheter i protokollspecifikationen. Implementeringar av nätverksprotokoll innehåller ofta kritiska buggar som kan utnyttjas. För att undvika buggar och sårbarheter måste implementeringar av nätverksprotokoll följa sina specifikationer. Målet med detta examensarbete är att använda symbolisk exekvering för att testa en implementation av protokollet Ephemeral Diffie-Hellman Over COSE ( EDHOC ) och en implementation av protokollet Constrained Application Protocol (CoAP) mot deras specifikationer. Syftet är att identifiera buggar såsom krascher, icke-konformiteter, minnesfel och säker-hetssårbarheter som kan uppstå om implementeringarna inte följer sina specifikationer. Metodiken för att uppnå detta består av tre steg: 1) extrahera krav från protokollensspecifikationer och uttrycka dem som formler, 2) förbereda systemet som ska testas försymbolisk exekvering och tillämpa formlerna under symbolisk exekvering för att upp-täcka eventuella vägar som bryter mot ett krav, 3) för varje väg som bryter mot ett krav används det konkreta värde som den symboliska exekveringsmotorn tillhandahåller i den oförändrade implementationen för att validera buggen. Totalt sett hittades sju icke-konformiteter. En icke-konformitet hittades i EDHOC implementeringen och sex hittades i CoAP implementeringen.