scholarly journals SAT and SMT-Based Verification of Security Protocols Including Time Aspects

Sensors ◽  
2021 ◽  
Vol 21 (9) ◽  
pp. 3055
Author(s):  
Sabina Szymoniak ◽  
Olga Siedlecka-Lamch ◽  
Agnieszka M. Zbrzezny ◽  
Andrzej Zbrzezny ◽  
Miroslaw Kurkowski
Keyword(s):  
Secure Communication ◽  
Formal Model ◽  
Timed Automata ◽  
Security Protocols ◽  
Communication Security ◽  
Huge Amount ◽  
Verification Methods ◽  
Security Property ◽  
Proper Operation ◽  
Timed Properties

For many years various types of devices equipped with sensors have guaranteed proper work in a huge amount of machines and systems. For the proper operation of sensors, devices, and complex systems, we need secure communication. Security protocols (SP) in this case, guarantee the achievement of security goals. However, the design of SP is not an easy process. Sometimes SP cannot realise their security goals because of errors in their constructions and need to be investigated and verified in the case of their correctness. Now SP uses often time primitives due to the necessity of security dependence on the passing of time. In this work, we propose and investigate the SAT-and SMT-based formal verification methods of SP used in communication between devices equipped with sensors. For this, we use a formal model based on networks of communicating timed automata. Using this, we show how the security property of SP dedicated to the sensors world can be verified. In our work, we investigate such timed properties as delays in the network and lifetimes. The delay in the network is the lower time constraint related to sending the message. Lifetime is an upper constraint related to the validity of the timestamps generated for the transmitted messages.

scholarly journals IMSC-EIoTD: Identity Management and Secure Communication for Edge IoT Devices

Sensors ◽  
2020 ◽  
Vol 20 (22) ◽  
pp. 6546
Author(s):  
Kazi Masum Sadique ◽  
Rahim Rahmani ◽  
Paul Johannesson
Keyword(s):  
Secure Communication ◽  
Identity Management ◽  
Security Protocols ◽  
Spin Model ◽  
The Internet ◽  
Human Society ◽  
Proposed Model ◽  
Authentication And Authorization ◽  
Quality Of Living ◽  
Iot Devices

The Internet of things (IoT) will accommodate several billions of devices to the Internet to enhance human society as well as to improve the quality of living. A huge number of sensors, actuators, gateways, servers, and related end-user applications will be connected to the Internet. All these entities require identities to communicate with each other. The communicating devices may have mobility and currently, the only main identity solution is IP based identity management which is not suitable for the authentication and authorization of the heterogeneous IoT devices. Sometimes devices and applications need to communicate in real-time to make decisions within very short times. Most of the recently proposed solutions for identity management are cloud-based. Those cloud-based identity management solutions are not feasible for heterogeneous IoT devices. In this paper, we have proposed an edge-fog based decentralized identity management and authentication solution for IoT devices (IoTD) and edge IoT gateways (EIoTG). We have also presented a secure communication protocol for communication between edge IoT devices and edge IoT gateways. The proposed security protocols are verified using Scyther formal verification tool, which is a popular tool for automated verification of security protocols. The proposed model is specified using the PROMELA language. SPIN model checker is used to confirm the specification of the proposed model. The results show different message flows without any error.

RDTA

2014 ◽  
Vol 5 (3) ◽  
pp. 42-67
Author(s):  
Fateh Latreche ◽  
Faiza Belala
Keyword(s):  
Web Services ◽  
Real Time ◽  
Formal Model ◽  
Timed Automata ◽  
Web Services Composition ◽  
Composite Service ◽  
The Real ◽  
Services Composition ◽  
Dynamic Web ◽  
Natural Way

Web services are very dynamic, they are all around us and we use them every day without even knowing it. In this paper, the authors define a formal model for dynamic Web services composition and they investigate how it can be used to specify and analyse backward recovery procedures, updating partner services in case of failure. First, they propose Recursive and Dynamic Timed Automata (RDTA) model, interpreted over composite service configurations, which provide a natural way to design stateful and dynamic Web services. Then, the authors define the concurrent semantics of this timed automata extension in terms of real-time rewrite theories. Analysis of the model is carried out in the Real-Time Maude system, based on checking relevant properties.

scholarly journals Formal analysis of security protocols for wireless sensor networks

2010 ◽  
Vol 47 (1) ◽  
pp. 81-97 ◽  
Author(s):  
Marián Novotný
Keyword(s):  
Sensor Networks ◽  
Formal Model ◽  
Formal Analysis ◽  
Security Protocols ◽  
Data Integrity ◽  
Wireless Sensor ◽  
Semantic Model ◽  
Communication Graph ◽  
Pi Calculus ◽  
Security Properties

Abstract Design of security protocols is notoriously error-prone. For this reason, it is required to use formal methods to analyze their security properties. In the paper we present a formal analysis of the Canvas protocol. The Canvas protocol was developed by Harald Vogt and should provide data integrity inWireless Sensor Networks. However, Dieter Gollmann published an attack on the protocol. We consider the fallacy of the Canvas scheme in different models of the attacker and present a solution for correcting the scheme.We propose a formal model of the fixed Canvas protocol in the applied pi-calculus. This model includes a model of the network topology, communication channels, captured nodes, and capabilities of the attacker. Moreover, we formulate and analyze the data integrity property of the scheme in the semantic model of the applied pi-calculus. We prove that the fixed Canvas scheme, in the presence of an active adversary, provides data integrity of messages assuming that captured nodes are not direct neighbors in the communication graph of a sensor network. Finally, we discuss the applicability of the proposed formal model for analysis of other WSN security protocols.

scholarly journals Efficient Temporal-key Based Encryption Mechanism for WSN-ETEM

2020 ◽  
Vol 9 (5) ◽  
pp. 143-148
Keyword(s):  
Key Management ◽  
Secure Communication ◽  
Energy Savings ◽  
Security Protocols ◽  
Packet Transmission ◽  
Sensor Nodes ◽  
Security And Privacy ◽  
Computational Overhead ◽  
Secure Data Transmission ◽  
Additional Support

Wireless sensor networks (WSNs) are a promising technology for several industrial real-time and quotidian applications. Due to inherent limitations in WSN, security is a crucial issue. Cryptographic primitives are the fundamental components for designing security protocols to achieve security and privacy in WSN. Based on the review, it has been analyzed that the majority of security protocols for WSN are based on encryption and key distribution. The main open issue for these approaches concerns the establishment of security with an involvement of complex procedure, which presents considerable memory overheads, in contrast with the limited resources of sensor nodes. Therefore, the proposed work presents the modeling of an analytical approach for efficient encryption using temporal key management for robust security services to resists potential attacks and enables secure communication. The utilization of temporal-key mechanism in encryption operation offers additional support to routing operation in the network for secure data transmission with negligible computational overhead, thus preserving a higher level of energy savings in packet transmission operation. The validation of the proposed system performance is carried out a simulation study, which shows the effectiveness of the proposed system in terms of node remaining energy and processing time.

Security Standards and Issues for Grid Computing

2012 ◽  
pp. 1656-1671
Author(s):  
Athanasios Moralis ◽  
Vassiliki Pouli ◽  
Mary Grammatikou ◽  
Dimitrios Kalogeras ◽  
Vasilis Maglaris
Keyword(s):  
Web Service ◽  
Secure Communication ◽  
Identity Management ◽  
Service Oriented Architecture ◽  
Security Protocols ◽  
Security Technologies ◽  
Security Environment ◽  
Grid Environments ◽  
Service Oriented ◽  
Security Standards

Security in grid environments that are built using Service Oriented Architecture (SOA) technologies is a great challenge. On one hand, the great diversity in security technologies, mechanisms and protocols that each organization follows and on the other hand, the different goals and policies that these organizations adopt, comprise a complex security environment. Authenticating and authorizing users and services, identity management in a multi-organizational scenario and secure communication define the main context of the problem. In this chapter, we provide an overview of the security protocols and technologies that can be applied on a Web Service (WS) based grid environment.

scholarly journals Blockchain and its Role in the Internet of Things (IoT)

2020 ◽  
Author(s):  
Tanweer Alam
Keyword(s):  
Internet Of Things ◽  
Secure Communication ◽  
Embedded Sensors ◽  
Smart Devices ◽  
Communication Security ◽  
The Internet ◽  
Novel Technology ◽  
Hash Code ◽  
The Internet Of Things

<p>Blockchain (BC) in the Internet of Things (IoT) is a novel technology that acts with decentralized, distributed, public and real-time ledger to store transactions among IoT nodes. A blockchain is a series of blocks, each block is linked to its previous blocks. Every block has the cryptographic hash code, previous block hash, and its data. The transactions in BC are the basic units that are used to transfer data between IoT nodes. The IoT nodes are different kind of physical but smart devices with embedded sensors, actuators, programs and able to communicate with other IoT nodes. The role of BC in IoT is to provide a procedure to process secured records of data through IoT nodes. BC is a secured technology that can be used publicly and openly. IoT requires this kind of technology to allow secure communication among IoT nodes in heterogeneous environment. The transactions in BC could be traced and explored through anyone who are authenticated to communicate within the IoT. The BC in IoT may help to improve the communication security. In this paper, I explored this approach, its opportunities and challenges. </p>

scholarly journals Blockchain and its Role in the Internet of Things (IoT)

2019 ◽  
pp. 151-157 ◽  
Author(s):  
Tanweer Alam
Keyword(s):  
Internet Of Things ◽  
Secure Communication ◽  
Embedded Sensors ◽  
Smart Devices ◽  
Communication Security ◽  
The Internet ◽  
Novel Technology ◽  
Hash Code ◽  
The Internet Of Things

Blockchain (BC) in the Internet of Things (IoT) is a novel technology that acts with decentralized, distributed, public and real-time ledger to store transactions among IoT nodes. A blockchain is a series of blocks, each block is linked to its previous blocks. Every block has the cryptographic hash code, previous block hash, and its data. The transactions in BC are the basic units that are used to transfer data between IoT nodes. The IoT nodes are different kind of physical but smart devices with embedded sensors, actuators, programs and able to communicate with other IoT nodes. The role of BC in IoT is to provide a procedure to process secured records of data through IoT nodes. BC is a secured technology that can be used publicly and openly. IoT requires this kind of technology to allow secure communication among IoT nodes in heterogeneous environment. The transactions in BC could be traced and explored through anyone who are authenticated to communicate within the IoT. The BC in IoT may help to improve the communication security. In this paper, I explored this approach, its opportunities and challenges.

scholarly journals Modeling and Verifying the CKB Blockchain Consensus Protocol

Mathematics ◽  
2021 ◽  
Vol 9 (22) ◽  
pp. 2954
Author(s):  
Meng Sun ◽  
Yuteng Lu ◽  
Yichun Feng ◽  
Qi Zhang ◽  
Shaoying Liu
Keyword(s):  
Knowledge Base ◽  
Formal Model ◽  
Timed Automata ◽  
Common Knowledge ◽  
Consensus Protocol

The Nervos CKB (Common Knowledge Base) is a public permissionless blockchain designed for the Nervos ecosystem. The CKB consensus protocol is the key protocol of the Nervos CKB, which improves the limit of the consensus’s performance for Bitcoin. In this paper, we developed the formal model of the CKB consensus protocol using timed automata. Based on the model, we formally verified various important properties of the Nervos CKB to provide a sufficient trustworthiness assurance. Especially, the security of the Nervos CKB against the selfish mining attacks to the protocol was investigated.

scholarly journals Efficient and Secure NFC Authentication for Mobile Payment Ensuring Fair Exchange Protocol

Symmetry ◽  
2020 ◽  
Vol 12 (10) ◽  
pp. 1649
Author(s):  
Chalee Thammarat
Keyword(s):  
Near Field ◽  
Mutual Authentication ◽  
Security Protocols ◽  
Internet Security ◽  
Fair Exchange ◽  
Formal Proofs ◽  
Session Key ◽  
Security Properties ◽  
Transaction Security ◽  
Security Property

The standard protocol of near field communication (NFC) has concentrated primarily on the speed of communication while ignoring security properties. Message between an NFC-enabled smartphone and a point of sale are exchanged over the air (OTA), which is a message considered an authentication request for payment, billing, ticketing, loyalty services, identification or access control. An attacker who has an antenna can intercept or manipulate the exchanged messages to take advantage of these. In order to solve this problem, many researchers have suggested authentication methods for NFC communications. However, these remain inadequate transaction security and fairness. In this paper, we will propose a technique that ensures mutual authentication, security properties, and strong fairness. Mutual authentication is a security property that prevents replay attacks and man-in-the-middle attacks. Both fair exchange and transaction security are also significant issues in electronic transactions with regards to creating trust among the parties participating in the transaction. The suggested protocol deploys a secure offline session key generation technique to increase transaction security and, importantly, make our protocol lightweight while maintaining the fairness property. Our analysis suggests that our protocol is more effective than others regarding transaction security, fairness, and lightweight protocol. The proposed protocol checks robustness and soundness using Burrows, Abadi and Needham (BAN) logic, the Scyther tool, and automated validation of internet security protocols and applications (AVISPA) that provide formal proofs for security protocols. Furthermore, our protocol can resolve disputes in case one party misbehaves.

Sign in / Sign up

Export Citation Format

Share Document