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.
|
PDF
1MB |
| 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: | https://purl.utwente.nl/essays/97069 |
| Export this item as: | BibTeX EndNote HTML Citation Reference Manager |
Show download statistics for this publication
Show download statistics for this publicationRepository Staff Only: item control page