BZPEERPapers, people, evidence and research pathsDiscover
Research tools
Network
Opportunities
Account
Source author record
Ender Yüksel appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.
Catalog footprint
Research graph
Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.
BZPEER is loading the nearby papers, people, topics and institutions for this page.
Published work
In this document, we present our applied results on balancing security and performance using a running example, which is based on sensor networks. These results are forming a basis for a new approach to balance security and performance, and therefore provide design-efficiency of key updates. We employ probabilistic model checking approach and present our modelling and analysis study using PRISM model checker.
In this report, we present our approach for protocol analysis together with a real example where we find an important flow in a contemporary wireless sensor network security protocol. We start by modelling protocols using a specific process algebraic formalism called LySa process calculus. We then apply an analysis based on a special program analysis technique called control flow analysis. We apply this technique to the ZigBee-2007 End-to-End Application Key Establishment Protocol and with the help of the analysis discover an unknown flaw. Finally we suggest a fix for the protocol, and verify that the fix works by using the same technique.
Cyber-physical systems integrate information and communication technology functions to the physical elements of a system for monitoring and controlling purposes. The conversion of traditional power grid into a smart grid, a fundamental example of a cyber-physical system, raises a number of issues that require novel methods and applications. In this context, an important issue is the verification of certain quantitative properties of the system. In this technical report, we consider a specific Chinese Smart Grid implementation and try to address the verification problem for certain quantitative properties including performance and battery consumption. We employ stochastic model checking approach and present our modelling and analysis study using PRISM model checker.
ZigBee is a fairly new but promising wireless sensor network standard that offers the advantages of simple and low resource communication. Nevertheless, security is of great concern to ZigBee, and enhancements are prescribed in the latest ZigBee specication: ZigBee-2007. In this technical report, we identify an important gap in the specification on key updates, and present a methodology for determining optimal key update policies and security parameters. We exploit the stochastic model checking approach using the probabilistic model checker PRISM, and assess the security needs for realistic application scenarios.