University of Twente Student Theses


Formal Verification of Lightweight Decentralized Attribute-based Encryption

Oosterhout, Janneke van (2023) Formal Verification of Lightweight Decentralized Attribute-based Encryption.

[img] PDF
Abstract:Attribute-based Encryption (ABE) is a public key cryptography scheme that provides one-to-many encryption. Decentralized Attribute-based Encryption (DABE) is a recent extension of ABE that does not have a single central authority (CA). DABE contains some heavy computations in the encryption algorithm, which prevents DABE from being implemented in many resource-constrained devices smoothly. Lightweight DABE versions are designed to perform efficiently on resource-constrained devices. Outsourcing (Outsourced Decentralized Attributebased Encryption (ODABE)) is an approach for lightweight encryption in DABE. Until now, there did not exist an outsourcing decryption scheme. Formal verification can be used to show that a cryptographic protocol meets its security properties. Formal verification can be done either by hand or by using an automated tool. Automated formal verification is a kind of Computer-aided Cryptography (CAC) and performs machine-checkable approaches to test the security of a protocol. There are numerous tools that perform automated verification, Tamarin is such an automated formal verification tool. To formally verify ODABE Tamarin is used. Security properties are modelled and it is proven that they hold in the model.
Item Type:Essay (Master)
Faculty:EEMCS: Electrical Engineering, Mathematics and Computer Science
Subject:54 computer science
Programme:Computer Science MSc (60300)
Link to this item:
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page