scholarly journals Model Checking M2M and Centralised IOT authentication Protocols.

2022 ◽  
Vol 2161 (1) ◽  
pp. 012042
Author(s):  
H Rekha ◽  
M. Siddappa
Keyword(s):  
Model Checking ◽  
High Reliability ◽  
Security Protocols ◽  
Authentication Protocol ◽  
Good Choice ◽  
Security Protocol ◽  
Security Requirements ◽  
Authentication Protocols ◽  
Security Properties ◽  
Functional Correctness

Abstract It is very difficult to develop a perfect security protocol for communication over the IoT network and developing a reliable authentication protocol requires a detailed understanding of cryptography. To ensure the reliability of security protocols of IoT, the validation method is not a good choice because of its several disadvantages and limitations. To prove the high reliability of Cryptographic Security Protocols(CSP) for IoT networks, the functional correctness of security protocols must be proved secure mathematically. Using the Formal Verification technique we can prove the functional correctness of IoT security protocols by providing the proofs mathematically. In this work, The CoAP Machine to Machine authentication protocol and centralied IoT network Authentication Protocol RADIUS is formally verified using the well-known verification technique known as model checking technique and we have used the Scyther model checker for the verification of security properties of the respective protocols. The abstract protocol models of the IoT authentication protocols were specified in the security protocol description language and the security requirements of the authentication protocols were specified as claim events.

A Secure Authentication Infrastructure for Mobile Users

2011 ◽  
pp. 56-80
Author(s):  
Gregor V. Bochmann ◽  
Eric Zhen Zhang
Keyword(s):  
Electronic Commerce ◽  
Authentication Protocol ◽  
Security Requirements ◽  
Mobile Users ◽  
Authentication Protocols ◽  
Its Analysis ◽  
Trust Relationships ◽  
Authentication Schemes ◽  
Access Rights ◽  
Secure Authentication

The requirements for an authentication infrastructure for electronic commerce are explained by identifying the partners involved in e-commerce transactions and the trust relationships required. Related security requirements are also explained, such as authentication, access rights, payment credentials, anonymity (in certain cases), and privacy and integrity of message exchanges. Then several general authentication schemes and specific protocols are reviewed and their suitability for mobile users is discussed. Finally, an improved authentication protocol is presented which can provide trust relationships for mobile e-commerce users. Its analysis and comparison with other proposed authentication protocols indicate that it is a good candidate for use in the context of mobile e-commerce.

scholarly journals Proving authentication property of PUF-based mutual authentication protocol based on logic of events

2021 ◽  
Author(s):  
Jiawen Song ◽  
Meihua Xiao ◽  
Tong Zhang ◽  
Haoyang Zhou
Keyword(s):  
Protocol Analysis ◽  
Mutual Authentication ◽  
Hardware Security ◽  
Authentication Protocol ◽  
Interaction Process ◽  
Authentication Protocols ◽  
Analysis Process ◽  
Security Properties ◽  
And Behavior ◽  
Mutual Authentication Protocol

AbstractPUF (Physical unclonable function) is a new hardware security primitive, and the research on PUFs is one of the emerging research focuses. For PUF-based mutual authentication protocols, a method to abstract the security properties of hardware by using logic of events is proposed, and the application aspects of logic of events are extended to protocols based on hardware security. With the interaction of PUF-based mutual authentication protocol formally described by logic of events, the basic sequences are constructed and the strong authentication property in protocol interaction process is verified. Based on the logic of events, the freshness of nonces is defined, and the persist rule is proposed according to the concept of freshness, which ensures the consistency of the protocol state and behavior predicate in the proof process, and reduces the complexity and redundancy in the protocol analysis process. Under reasonable assumptions, the security of the protocol is proven, and the fact that logic of events applies to PUF-based mutual authentication protocols is shown.

scholarly journals Wireless Authentication in chi-Spaces

2003 ◽  
Vol 10 (10) ◽  
Author(s):  
Federico Crazzolara ◽  
Giuseppe Milicia
Keyword(s):  
Life Cycle ◽  
Low Power ◽  
Programming Language ◽  
Security Protocols ◽  
Authentication Protocol ◽  
Security Protocol ◽  
Wireless Devices ◽  
Formal Calculus

The chi-Spaces framework provides a set of tools to support every step of the security protocol's life-cycle. The framework includes a simple, yet powerful programming language which is an implementation of the Security Protocol Language (SPL). SPL is a formal calculus designed to model security protocols and prove interesting properties about them. In this paper we take an authentication protocol suited for low-power wireless devices and derive a chi-Spaces implementation from its SPL model. We study the correctness of the resulting implementation using the underlying SPL semantics of chi-Spaces.

A Secure Authentication Infrastructure for Mobile Users

2008 ◽  
pp. 3765-3783
Author(s):  
Gregor V. Bochmann ◽  
Eric Zhen Zhang
Keyword(s):  
Electronic Commerce ◽  
Authentication Protocol ◽  
Security Requirements ◽  
Mobile Users ◽  
Authentication Protocols ◽  
Its Analysis ◽  
Trust Relationships ◽  
Authentication Schemes ◽  
Access Rights ◽  
Secure Authentication

The requirements for an authentication infrastructure for electronic commerce are explained by identifying the partners involved in e-commerce transactions and the trust relationships required. Related security requirements are also explained, such as authentication, access rights, payment credentials, anonymity (in certain cases), and privacy and integrity of message exchanges. Then several general authentication schemes and specific protocols are reviewed and their suitability for mobile users is discussed. Finally, an improved authentication protocol is presented which can provide trust relationships for mobile e-commerce users. Its analysis and comparison with other proposed authentication protocols indicate that it is a good candidate for use in the context of mobile e-commerce.

scholarly journals Formal Verification of CHAP PPP authentication Protocol for Smart City/Safe City Applications.

2022 ◽  
Vol 2161 (1) ◽  
pp. 012046
Author(s):  
R Pradeep ◽  
N R Sunitha
Keyword(s):  
Formal Verification ◽  
Smart City ◽  
Smart Cities ◽  
Mathematical Proof ◽  
Security Protocols ◽  
Authentication Protocol ◽  
Security Protocol ◽  
Metropolitan Region ◽  
Security Systems ◽  
Point To Point

Abstract A smart city is a technologically advanced metropolitan region with several connected devices that collects data using various electronic technologies, voice activation methods, and sensors. The information obtained from the data is utilised to efficiently manage assets, resources, and services; in turn, the data is used to enhance operations throughout the city. Achieving security for smart cities is one of the major challenges as the number of connected devices increases the vulnerability also increases. The security of a smart city system depends on the reliability of the security protocols used by the security systems. To design and develop a highly secure system for a smart city the security protocols used must be highly reliable. To prove the reliability of a security protocol the validation technique is not desirable because of its several drawbacks, these drawbacks can be overcome using the formal verification technique which provides the mathematical proof for its correctness. In this work, The Challenge-Handshake Authentication Protocol Point-to-Point (CHAP PPP) which is more commonly used in PPP authentication of smart cities is formally verified using the well-known verification technique known as the model checking technique. The Scyther model checker is the tool used to build the abstract security protocol model.

Modeling of Wireless Network Security Authentication Protocol Based on SPIN

2013 ◽  
Vol 336-338 ◽  
pp. 1892-1897
Author(s):  
Li Zhou ◽  
Fang Yong Tan
Keyword(s):  
Network Security ◽  
Model Checking ◽  
Wireless Network ◽  
Authentication Protocol ◽  
Security Vulnerabilities ◽  
Wireless Network Security ◽  
Security Authentication ◽  
Security Properties ◽  
Authentication Security ◽  
Network Authentication

It’s important to insure wireless network authentication security. Via model checking tool SPIN modeling 802.1x EAP-TLS authentication protocol, communication parts are defined with model checking language PROMELA, security properties are expressed by LTL formula, and the model is verified. With the attack track given by SPIN, the security vulnerabilities caused by the improper configuration is pointed out, meanwhile the new tunnel authentication protocol is proposed to reduce the occurrence of attack and to improve the agreement.

scholarly journals Events in Security Protocols

2001 ◽  
Vol 8 (13) ◽  
Author(s):  
Federico Crazzolara ◽  
Glynn Winskel
Keyword(s):  
Petri Nets ◽  
Expressive Language ◽  
Security Protocols ◽  
Security Protocol ◽  
Event Structures ◽  
Restricted Form ◽  
Wide Range ◽  
Strand Spaces ◽  
Security Properties ◽  
Event Based

<p>The events of a security protocol and their causal dependency<br />can play an important role in the analysis of security properties.<br /> This insight underlies both strand spaces and the inductive<br />method. But neither of these approaches builds up the events of<br />a protocol in a compositional way, so that there is an informal<br />spring from the protocol to its model. By broadening the models<br />to certain kinds of Petri nets, a restricted form of contextual nets,<br />a compositional event-based semantics is given to an economical,<br />but expressive, language for describing security protocols; so the<br />events and dependency of a wide range of protocols are determined<br /> once and for all. The net semantics is formally related to a<br />transition semantics, strand spaces and inductive rules, as well as<br />trace languages and event structures, so unifying a range of <br />approaches, as well as providing conditions under which particular,<br />more limited, models are adequate for the analysis of protocols.<br />The net semantics allows the derivation of general properties and<br />proof principles which are demonstrated in establishing an <br />authentication property, following a diagrammatic style of proof.</p>

scholarly journals Modified Authentication Protocol and Evaluation Tool: Kerberos and BAN Logic

2019 ◽  
Vol 8 (3) ◽  
pp. 2432-2436
Keyword(s):  
Computer Network ◽  
Exchange Process ◽  
Security Protocols ◽  
Authentication Protocol ◽  
Ban Logic ◽  
Secret Key ◽  
Evaluation Tool ◽  
Authentication Protocols ◽  
Online Transactions ◽  
Physical Address

In today’s world the computer network communication increases the efficiency most of the organizations. Hence threats have been increased due to these online transactions/communications. These threats necessitate the researchers to improve the existing security protocols and /or develop the new ones. Authentication Protocols are one of the same which can provide the authentication, confidentiality & integrity. For checking the authenticity of messages exchange process in authentication protocols BAN logic is used. The Kerberos encrypt the information for authentications. Many organizations use it and it has five versions and versions 4 and 5 are latest. In one of over previous paper we have generalized the ticket exchange process of version 5. In this paper to make it more authenticated some modifications are proposed to both BAN and Kerberos and we defined them as R- Kerberos & RBAN. To achieve this, we have added participant’s physical address (MAC Address) as it is unique to every network adapter and can be used as our secret key.

scholarly journals Lessons Learned: Analysis of PUF-based Authentication Protocols for IoT

2021 ◽  
Author(s):  
Karim Lounis ◽  
Mohammad Zulkernine
Keyword(s):  
Low Cost ◽  
Lessons Learned ◽  
Security Requirements ◽  
Authentication Protocols ◽  
Physical Unclonable Functions ◽  
Security Issues ◽  
Cryptographic Keys ◽  
Security Properties ◽  
The Subject ◽  
Lightweight Authentication

The service of authentication constitutes the spine of all security properties. It is the phase where entities prove their identities to each other and generally establish and derive cryptographic keys to provide confidentiality, data integrity, non-repudiation, and availability. Due to the heterogeneity and the particular security requirements of IoT (Internet of Things), developing secure, low-cost, and lightweight authentication protocols has become a serious challenge. This has excited the research community to design and develop new authentication protocols that meet IoT requirements. A recent technology, called PUFs (Physical Unclonable Functions), has been the subject of many subsequent publications on lightweight, low-cost, and secure-by-design authentication protocols. This has turned our attention to investigate the most recent PUF-based authentication protocols for IoT. In this paper, we review the security of these protocols. We first provide the necessary background on PUFs, their types, and related attacks. Also, we discuss how PUFs are used for authentication. Then, we analyze the security of PUF-based authentication protocols to identify and report common security issues and design flaws, as well as to provide recommendations for future authentication protocol designers.

"Recent Patents on the Triboelectrostatic Separation of Fly Ash"

2019 ◽  
Vol 13 ◽  
Author(s):  
Haisheng Li ◽  
Wenping Wang ◽  
Yinghua Chen ◽  
Xinxi Zhang ◽  
Chaoyong Li
Keyword(s):  
Fly Ash ◽  
Power Plants ◽  
High Efficiency ◽  
Separation Efficiency ◽  
High Reliability ◽  
Operating Conditions ◽  
Security Requirements ◽  
Unburned Carbon ◽  
Efficient Operation ◽  
Triboelectrostatic Separation

Background: The fly ash produced by coal-fired power plants is an industrial waste. The environmental pollution problems caused by fly ash have been widely of public environmental concern. As a waste of recoverable resources, it can be used in the field of building materials, agricultural fertilizers, environmental materials, new materials, etc. Unburned carbon content in fly ash has an influence on the performance of resource reuse products. Therefore, it is the key to remove unburned carbon from fly ash. As a physical method, triboelectrostatic separation technology has been widely used because of obvious advantages, such as high-efficiency, simple process, high reliability, without water resources consumption and secondary pollution. Objective: The related patents of fly ash triboelectrostatic separation had been reviewed. The structural characteristics and working principle of these patents are analyzed in detail. The results can provide some meaningful references for the improvement of separation efficiency and optimal design. Methods: Based on the comparative analysis for the latest patents related to fly ash triboelectrostatic separation, the future development is presented. Results: The patents focused on the charging efficiency and separation efficiency. Studies show that remarkable improvements have been achieved for the fly ash triboelectrostatic separation. Some patents have been used in industrial production. Conclusion: According to the current technology status, the researches related to process optimization and anti-interference ability will be beneficial to overcome the influence of operating conditions and complex environment, and meet system security requirements. The intelligent control can not only ensure the process continuity and stability, but also realize the efficient operation and management automatically. Meanwhile, the researchers should pay more attention to the resource utilization of fly ash processed by triboelectrostatic separation.

Sign in / Sign up

Export Citation Format

Share Document