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

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.

Model Checking M2M and Centralised IOT authentication Protocols.

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 Scalable Security Protocol for Intravehicular Controller Area Network

Intravehicular communication relies on controller area network (CAN) protocol to deliver messages and instructions among different electronic control units (ECU). Unfortunately, inherent defects in CAN include the absence of confidentiality and integrity mechanism, enabling adversaries to launch attacks from wired or wireless interfaces. Although various CAN cryptographic protocols have been proposed for entity authentication and secure communication, the redundancy in the key establishment phase weakens their availability in large-scale CAN. In this paper, we propose a scalable security protocol suite for intravehicular networks and reduce the communication costs significantly. A new type of attack, suspension attack, is identified for the existing protocols and mitigated in our protocol by leveraging a global counter scheme. We formally verify the security properties of the proposed protocol suite through the AVISPA tool. The simulation results indicate that the communication and computation efficiency are improved in our protocol.

Xây dựng giải pháp trao đổi khóa IKEv2 sử dụng NIOS II trên FPGA

Tóm tắt—Giao thức Internet Key Exchange (IKE) là một giao thức thực hiện quá trình trao đổi khóa và thỏa thuận trong chế độ bảo mật IPSec. Để thực thi giao thức bảo mật IPSec tốc độ cao thì thường kết hợp giữa phần mềm và phần cứng trên vi mạch Field Programmable Gate Array (FPGA) [7], [8]. Trong đó, các thao tác mật mã, đóng gói và bóc tách gói tin được thực hiện bằng FPGA để đảm bảo thực hiện hệ thống IPSec tốc độ cao; giao thức trao đổi khóa IKE được thực hiện bằng phần mềm sử dụng hệ điều hành Linux nhúng. Trong bài báo này, nhóm tác giả giới thiệu giải pháp thực hiện giải thuật trao đổi khóa IKE sử dụng Nios II trên FPGA. Với cách tiếp cận này, nhóm tác giả đã tự tổ chức, xây dựng chương trình trên bộ vi xử lý, nhờ đó kiểm soát được toàn bộ dòng dữ liệu. Abstract—IKE (Internet Key Exchange) is a protocol that performs key exchange and agreement process in IPSec security mode. To implement high speed IPSec security protocol, it is often combined software and hardware on Field Programmable Gate Array (FPGA) [7], [8]. Therein, encryption, packet encapsulation and extraction operations will be performed by FPGA to ensure high speed IPSec system implementation; the IKE protocol is implemented by software using an embed Linux operating system. In this paper, the authors introduce the solution of implementing IKE key exchange algorithm using Nios II on FPGA. With this approach, the authors have organized and built the program on the microprocessor by themselves, therefore the entire data stream is controlled.

Security and Privacy for Edge-Assisted Internet of Things Security Proof for the SKKE Protocol

As an Internet of things (IoT) technology, the ZigBee has a wide range of applications in home automation, smart energy, commercial building automation, personal, home and hospital care, telecom, and wireless sensor. The ZigBee standard has the advantage of high reliability, which is based on the security of authentication key agreement protocol, namely, the SKKE protocol. In the ZigBee standard, this protocol based on shared symmetric-key is applied on the security protocol level. It is a full symmetric-key key agreement with key confirmation scheme, while the key confirmation mechanism is provided by a message authentication coding mechanism. In this paper, we consider the security of the SKKE protocol. In the random Oracle model, we reduce the security of the SKKE protocol to the collision of the hash function and the HMAC function and the indistinguishability between the output of the random Oracle and a random number. We also give a theoretical proof with the game-based method. To our knowledge, there is no research on the provable security of the ZigBee protocol at this stage, so it is helpful to promote further research of the ZigBee protocol security.

Research on Security Protocol Analysis Tool SmartVerif

Security protocols have been designed to protect the security of the network. However, many security protocols cannot guarantee absolute security in real applications. Therefore, security tests of the network protocol become particularly important. In this paper, firstly, we introduce SmartVerif, which is the first formal analysis tool to automatically verify the security of protocols through dynamic strategies. And then, we use SmartVerif to verify the pseudo-randomness of the encapsulated key of the Two-Pass AKE protocol, which was proposed by Liu’s in ASIACRYPT in 2020. Finally, we summary our work and show some limitations of SmartVerif. At the same time, we also point out the direction for future improvement of SmartVerif.

RootLogChain: Registering Log-Events in a Blockchain for Audit Issues from the Creation of the Root

Logging system activities are required to provide credibility and confidence in the systems used by an organization. Logs in computer systems must be secured from the root user so that they are true and fair. This paper introduces RootLogChain, a blockchain-based audit mechanism that is built upon a security protocol to create both a root user in a blockchain network and the first log; from there, all root events are stored as logs within a standard blockchain mechanism. RootLogChain provides security constructs so as to be deployed in a distributed context over a hostile environment, such as the internet. We have developed a prototype based on a microservice architecture, validating it by executing different stress proofs in two scenarios: one with compliant agents and the other without. In such scenarios, several compliant and non-compliant agents try to become a root and register the events within the blockchain. Non-compliant agents simulate eavesdropper entities that do not follow the rules of the protocol. Our experiments show that the mechanism guarantees the creation of one and only one root user, integrity, and authenticity of the transactions; it also stores all events generated by the root within a blockchain. In addition, for audit issues, the traceability of the transaction logs can be consulted by the root.