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
Protocol, mobility and adversary models for the verification of security
Uppsala universitet, Avdelningen för datorteknik.ORCID iD: 0000-0001-9645-1129
2016 (English)Licentiate thesis, comprehensive summary (Other academic)
Abstract [en]

The increasing heterogeneity of communicating devices, ranging from resource constrained battery driven sensor nodes to multi-core processor computers, challenges protocol design. We examine security and privacy protocols with respect to exterior factors such as users, adversaries, and computing and communication resources; and also interior factors such as the operations, the interactions and the parameters of a protocol.

Users and adversaries interact with security and privacy protocols, and even affect the outcome of the protocols. We propose user mobility and adversary models to examine how the location privacy of users is affected when they move relative to each other in specific patterns while adversaries with varying strengths try to identify the users based on their historical locations. The location privacy of the users are simulated with the support of the K-Anonymity protection mechanism, the Distortion-based metric, and our models of users' mobility patterns and adversaries' knowledge about users.

Security and privacy protocols need to operate on various computing and communication resources. Some of these protocols can be adjusted for different situations by changing parameters. A common example is to use longer secret keys in encryption for stronger security. We experiment with the trade-off between the security and the performance of the Fiat–Shamir identification protocol. We pipeline the protocol to increase its utilisation as the communication delay outweighs the computation.

A mathematical specification based on a formal method leads to a strong proof of security. We use three formal languages with their tool supports in order to model and verify the Secure Hierarchical In-Network Aggregation (SHIA) protocol for Wireless Sensor Networks (WSNs). The three formal languages specialise on cryptographic operations, distributed systems and mobile processes. Finding an appropriate level of abstraction to represent the essential features of the protocol in three formal languages was central.

Place, publisher, year, edition, pages
Uppsala University , 2016. , p. 132
National Category
Computer Sciences Communication Systems
Research subject
Computer Science with specialization in Computer Communication
Identifiers
URN: urn:nbn:se:kth:diva-202017OAI: oai:DiVA.org:kth-202017DiVA: diva2:1075019
Presentation
2016-09-19, Uppsala, 10:15 (English)
Opponent
Supervisors
Projects
ProFuN
Note

QC 20170217

Available from: 2017-02-17 Created: 2017-02-16 Last updated: 2018-01-13Bibliographically approved
List of papers
1. The impact of trace and adversary models on location privacy provided by K-anonymity
Open this publication in new window or tab >>The impact of trace and adversary models on location privacy provided by K-anonymity
2012 (English)In: Proc. 1st Workshop on Measurement, Privacy, and Mobility, New York: ACM Press , 2012, article id 6Conference paper, Published paper (Refereed)
Abstract [en]

Privacy preserving mechanisms help users of location-based services to balance their location privacy while still getting useful results from the service. The provided location privacy depends on the users' behavior and an adversary's knowledge used to locate the users. The aim of this paper is to investigate how users' mobility patterns and adversaries' knowledge affect the location privacy of users querying a location-based service. We consider three mobility trace models in order to generate user traces that cross each other, are parallel to each other and form a circular shape. Furthermore, we consider four adversary models, which are distinguished according to their level of knowledge of users. We simulate the trace and the adversary models by using Distortion-based Metric and K-anonymity. The results show that the location privacy provided by K-anonymity decreases, as users are located closer to each other in the trace models. The impact of the adversary on location privacy is reduced as more users are cloaked together.

Place, publisher, year, edition, pages
New York: ACM Press, 2012
National Category
Computer Sciences
Research subject
Computer Science with specialization in Computer Communication
Identifiers
urn:nbn:se:kth:diva-202020 (URN)10.1145/2181196.2181202 (DOI)2-s2.0-84860731130 (Scopus ID)978-1-4503-1163-2 (ISBN)
Conference
MPM 2012
Projects
ProFuNWISENET
Note

QC 20170308

Available from: 2012-04-10 Created: 2017-02-16 Last updated: 2018-01-13Bibliographically approved
2. Towards adaptive zero-knowledge protocols: A case study with Fiat–Shamir identification protocol
Open this publication in new window or tab >>Towards adaptive zero-knowledge protocols: A case study with Fiat–Shamir identification protocol
2013 (English)In: Proc. 9th Swedish National Computer Networking Workshop, 2013, p. 67-70Conference paper, Published paper (Refereed)
Abstract [en]

Interactive zero-knowledge protocols are used as identification protocols. The protocols are executed in rounds, with security being increased with every round. This allows for a trade-off between security and performance to adapt the protocol to the requirements of the scenario. We experimentally investigate the Fiat–Shamir identification protocol on machines and networks with different performance characteristics. We find that the delay of the protocol highly depends on network latency and upload bandwidth. Computation time becomes more visible, when the protocol transmits little amount of data via a low latency network. We also experience that the impact of the sizes of the variables on the delay of the protocol is less than the number of rounds', which are interior factors in the protocol.

National Category
Computer Sciences
Research subject
Computer Science with specialization in Computer Communication
Identifiers
urn:nbn:se:kth:diva-202019 (URN)
Conference
SNCNW 2013
Projects
WISENETProFuN
Note

QC 20170308

Available from: 2013-06-05 Created: 2017-02-16 Last updated: 2018-01-13Bibliographically approved
3. Modelling and analysing a WSN secure aggregation protocol: A comparison of languages and tool support
Open this publication in new window or tab >>Modelling and analysing a WSN secure aggregation protocol: A comparison of languages and tool support
2015 (English)Report (Other academic)
Abstract [en]

A security protocol promises protection of a significant piece of information while using it for a specific purpose. Here, the protection of the information is vital and a formal verification of the protocol is an essential step towards guaranteeing this protection. In this work, we study a secure aggregation protocol (SHIA) for Wireless Sensor Networks and verify the protocol in three formal modelling tools (Pwb, mCRL2 and ProVerif). The results of formal verification heavily depend on the model specification and the ability of the tools to deal with the model. Among the three tools, there is difference in data representation, communication types and the level of abstraction in order to represent SHIA. ProVerif and mCRL2 are mature and well-established tools, geared respectively towards security and distributed systems; however, their expressiveness constrains modelling SHIA and its security properties. Pwb is an experimental tool developed by the authors; its relative immaturity is offset by its increased expressive power and customisability. This leads to different models of the same protocol, each contributing in different ways to our understanding of SHIA's security properties.

Place, publisher, year, edition, pages
Uppsala University, 2015
National Category
Computer Sciences Communication Systems
Research subject
Computer Science with specialization in Computer Communication
Identifiers
urn:nbn:se:kth:diva-202018 (URN)
Projects
ProFuN
Funder
Swedish Foundation for Strategic Research , RIT08-0065]
Note

QC 20170308

Available from: 2015-12-03 Created: 2017-02-16 Last updated: 2018-01-13Bibliographically approved

Open Access in DiVA

fulltext(9684 kB)13 downloads
File information
File name FULLTEXT01.pdfFile size 9684 kBChecksum SHA-512
7df0ecbdaa29fdfe018cf4bc289f2f9cd6524f1724047ec1a7b7b25fce846d6c174b964cfa46b14bda0da53a99db2766d64e7e5d8b5459fbcba0fe0a3798371f
Type fulltextMimetype application/pdf

Search in DiVA

By author/editor
Cambazoglu, Volkan
Computer SciencesCommunication Systems

Search outside of DiVA

GoogleGoogle Scholar
Total: 13 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: 45 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