Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Formalizing security properties in blockchain protocols
KTH, School of Electrical Engineering and Computer Science (EECS).
KTH, School of Electrical Engineering and Computer Science (EECS).
2018 (English)Independent thesis Basic level (degree of Bachelor), 10 credits / 15 HE creditsStudent thesisAlternative title
Formalisering av säkerhetsegenskaper i blockkedjeprotokoll (Swedish)
Abstract [en]

In this report we have used the logic L to write a formal specification of security properties in blockchain protocols for managing Electronic Health Records. The protocols have been adapted from previous research, and then formalized with regards to the properties data privacy and data integrity. We used the logic L to define a logical model M. M was then used to write formulas which formalize security properties in the blockchain protocols. The protocols handle encryption key exchange, agent authentication, permission handling and read/write operations to blockchain storage. It remains to be proven that the adapted protocols have the properties defined by our formal specification.

Abstract [sv]

I denna rapport använder vi logiken L för att skriva en formell specifikation för säkerhetsaspekter i blockkedjeprotokoll för patientjournaler. Vi använder logiken L för att definiera en logikmodell M och skriva formler som formaliserar säkerhetsaspekterna i blockkedjeprotokollen. Vår ansats är att formalisera aspekterna data privacy och data integrity för modifierade teoretiska protokol från tidigare forskning. Protokollen hanterar utbyte av krypteringsnycklar, agent-autentisiering, tillståndshantering samt läs- och skriv-operationer. Det återstår att bevisa att de modifierade protokollen har de egenskaper som definieras i vår formella specifikation.

Place, publisher, year, edition, pages
2018.
Series
TRITA-EECS-EX ; 2018:204
National Category
Computer Sciences
Identifiers
URN: urn:nbn:se:kth:diva-230642OAI: oai:DiVA.org:kth-230642DiVA, id: diva2:1217901
Subject / course
Computer Science
Supervisors
Examiners
Available from: 2018-06-26 Created: 2018-06-13 Last updated: 2018-06-26Bibliographically approved

Open Access in DiVA

fulltext(1505 kB)72 downloads
File information
File name FULLTEXT01.pdfFile size 1505 kBChecksum SHA-512
ad68f6e7a96a122c4212ec8d5970ac91b172e74907890f5dc70f96424a2aaccdb8bf0f6fb39a991f403d7a1952c8514c78ee015bd88df1ff0b93faa3c928bef2
Type fulltextMimetype application/pdf

By organisation
School of Electrical Engineering and Computer Science (EECS)
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar
Total: 72 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

urn-nbn

Altmetric score

urn-nbn
Total: 143 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf