In recent days, security and privacy is becoming a challenge due to the rapid development of technology. In 2021, Khan et al. proposed an authentication and key agreement framework for smart grid network and claimed that the proposed protocol provides security against all well-known attacks. However, in this paper, we present the analysis and shows that the protocol proposed by Khan et al has failed to protect the secrecy of the shared session key between the user and service provider. An adversary can derive the session key (online) by intercepting the communicated messages under the Dolev-Yao threat model. We simulated Khan et al.’s protocol for formal security verification using Tamarin Prover and found a trace for deriving the temporary key. It is used to encrypt the login request that includes the user’s secret credentials. Hence, it also fails to preserve the privacy of the user’s credentials, and therefore any adversary can impersonate the user. As a result, the protocol proposed by Khan et al. is not suitable for practical applications.

Protocol Verification - PCI Express (Peripheral Component Interconnect) is a point-to-point, high-performance, serial interconnect protocol. PCIe outperforms older buses and offers greater bandwidth, making it a fantastic option for a wide range of applications. PCIe features layered architecture with three distinct layers. Packets are used to convey information between these layers. The verification IP of the physical layer in PCI Express is implemented in this paper. The Universal Verification Methodology is used for development of VIP of PCIe, which is written in System Verilog (UVM).

Protocol Verification - Transactions involving multiple blockchains are implemented by cross-chain protocols. These protocols are based on smart contracts, programs that run on blockchains, executed by a network of computers. Verifying the runtime correctness of smart contracts is a problem of compelling practical interest since, smart contracts can automatically transfer ownership of cryptocurrencies, electronic securities, and other valuable assets among untrusting parties. Such verification is challenging since smart contract execution is time sensitive, and the clocks on different blockchains may not be perfectly synchronized. This paper describes a method for runtime monitoring of blockchain executions. First, we propose a generalized runtime verification technique for verifying partially synchronous distributed computations for the metric temporal logic (MTL) by exploiting bounded-skew clock synchronization. Second, we introduce a progression-based formula rewriting scheme for monitoring MTL specifications which employs SMT solving techniques and report experimental results.

Protocol Verification - As a new generation of high-performance chip-to-chip packet transmission protocol, Interlaken is usually embedded in FPGA, ARM, DSP and other chips in the way of IP core. As a high bandwidth network communication protocol, relevant testing and verification work is the key to support users highly reliable applications.This paper analyzes the framing layer and protocol layer of Interlaken IP core embedded in FPGA, encapsulates the pre-defined data at the client end of the protocol layer, tests the working condition under the transmission rate of 100Gbps, and error injection in one segment of the four-segment user-side to simulate packet encapsulation errors. The study found that when sending packets, when any control word in any segment is lost, about 1/2 of the packets are received and about 1/4 are received correctly.

Protocol Verification - Symbolic protocol verification generally abstracts probabilities away, considering computations that succeed only with negligible probability, such as guessing random numbers or breaking an encryption scheme, as impossible. This abstraction, sometimes referred to as the perfect cryptography assumption, has shown very useful as it simplifies automation of the analysis. However, probabilities may also appear in the control flow where they are generally not negligible. In this paper we consider a framework for symbolic protocol analysis with a probabilistic choice operator: the probabilistic applied pi calculus. We define and explore the relationships between several behavioral equivalences. In particular we show the need for randomized schedulers and exhibit a counterexample to a result in a previous work that relied on nonrandomized ones. As in other frameworks that mix both non-deterministic and probabilistic choices, schedulers may sometimes be unrealistically powerful. We therefore consider two subclasses of processes that avoid this problem. In particular, when considering purely non-deterministic protocols, as is done in classical symbolic verification, we show that a probabilistic adversary has—maybe surprisingly—a strictly superior distinguishing power for may testing, which, when the number of sessions is bounded, we show to coincide with purely possibilistic similarity.

Protocol Verification - Microservices is an architectural style that enables the design of applications as series of services independent from each other in function, maintainability, deployability and scalability. Two phase commit protocol as an example of classical distributed transaction protocols are not suitable for this pattern. These protocols require all participants in a transaction to commit or roll back before the transaction can proceed. This is way saga was chosen to replace 2PC. Saga is a mechanism that belongs to the ’database per service’ pattern and which guarantees distributed transactions that covers many services. The saga pattern provides transaction management using a sequence of local transactions. Saga can be rolled back by a compensating transaction that ensures one of two possibilities all operations complete successfully or the corresponding compensation transactions are run to undo the change. In this paper, we try to run a verification of saga using the maude language. We use the Saga protocol by orchestration, and we present a verification way to check it.

Protocol Verification - Bus protocols are critical for the operation of a system as all communications are handled through the bus by following a predetermined structure. An IP is designed to verify if the system follows the specified protocol for seamless communications between multiple blocks in the system. As the process technology decreases the number of sub-blocks in the system also increases thus the verification complexity increases. In Traditional verification architecture, the design under test (DUT) signals are individually connected to the verification environment by binding the interface to the subblocks, signals are encapsulated and simplified to handle. In this work, an AHB verification module is designed by employing the interface binding technique.

Protocol Verification - Attribute-based encryption (ABE) is an extension scheme of identity-based encryption and public-key encryption. It can achieve fine-grained access control and one-to-many encryption mode, suitable for practical applications. In addition to mathematical proofs, it is essential to verify its security properties using different protocols. This paper proposes two key exchange protocols to securely exchange the user secret keys in ABE. ProVerif is an automated cryptographic protocol verifier that we have used during protocol verification. We specifically aim to protect the confidentiality of the generated keys. The proposed protocols are formally analysed and their security property has been formally proved.

Protocol Verification - The System-On-Chip (SoC) designs are becoming more complex nowadays. Multiple Intellectual Property (IPs) are integrated in a single SoC and these IPs communicate with the help of various bus protocols. Verification takes almost 70 \% time in design cycle hence re-usable verification environment of these commonly used protocols is very important. In this paper, AXI4-Lite protocol is verified using UVM based testbench structure. To verify all channels of AX I protocol, data is written into a 4-bit shift register and it is read back. The UVM testbench acts as a master device which will send all control information, data and address to the register through the AXI interface. To understand verification goal achievement, coverpoints are written and functional and code coverage reports are analyzed. The synopsys V CS tool is used for the simulation.

Protocol Verification - Display Serial Interface (DSI) is a high-speed serial interface standard. It supports display and touch screens in mobile devices such as smartphones, laptops, tablets, and other platforms. DSI describes several layers that define the detailed interconnect between a host processor and a peripheral device in a mobile system. The targeted DSI protocol layer is the low-level layer in the standard which is responsible for bytes organization, error-checking information addition, and packet formulation. In this paper, we propose a constrained random Coverage-Driven Verification approach (CDV) for the DSI lowlevel protocol layer using Universal Verification Methodology (UVM). This approach could be the basis of a standardized Verification Intellectual Property (VIP) to test and verify the standardized DSI layer. We provide a well-established base of a reusable and scalable UVM environment that can verify the DSI protocol layer using various techniques such as error injection mechanism, System Verilog Assertions (SVA), and direct UVM sequences aim to cover the different real-life scenarios between the host processor and the peripheral device. Our results show that we can detect all inserted errors to assure the functionality of the DSI low-level protocol layer. Different real-life scenarios between the host processor and the peripheral device are covered with 100\% functional coverage and 93\% code coverage.

Operating Systems Security - The operating system is the core of the smart power terminal. It is designed to strengthen security from five aspects: terminal container security, system security, security audit, communication protocol security, and hardware access control. By formulating a verification strategy, a comparative security test was carried out for the security hardening and non-security hardening operating systems of smart power terminals, and a detailed comparison test table was formed, demonstrating the importance of security hardening and security hardening for the operating systems of smart power terminals The advantages. The security-hardened operating system can effectively ensure the security of the operating environment of the terminal body and prevent illegal access by malicious programs.

MANET Privacy - Various routing methods and approaches are being integrated into wireless networks, making it a topic for future investigation. The two primary wireless routing issues under research are security and congestion reduction. The bulk of security research relies on key-based approaches or third-party trust control systems. The routing protocol would be secured by validating a nonblocking identity, which is relayed to each site via protocol, according to the study's enhanced route security. Adhoc upon Request Vertical (AODV) connectivity is a dynamically routing technique that chooses the best route based on the databases of its neighbors. The research in this article emphasizes privacy for routing security, and simulators are given to show the improved delivery ratio, speed, end-to-end lag, and reduced packet loss rate of the Ad hoc On Requirement Done Accordingly (AODV) networking protocol. Attacks are deliberately avoided by modifying the basic implementation of the AODV networking protocol. Further suggestions made in this research include the deployment of an access control strategy and distinctive key-based verification for AODV. There is always a need for research in this area since security measures might have a detrimental influence on the functioning of the system in place. There is an urgent need for continued study in this area but since audiovisual and audio industries are growing quickly.

Internet-scale Computing Security - With the rapid growth of the number of global network entities and interconnections, the security risks of network relationships are constantly accumulating. As the basis of network interconnection and communication, Internet routing is facing severe challenges such as insufficient online monitoring capability of large-scale routing events and lack of effective and credible verification mechanism. Major global routing security events emerge one after another, causing extensive and far-reaching impacts. To solve these problems, China Telecom studied the BGP (border gateway protocol) SDN (software defined network) controller technology to monitor the interconnection routing, constructed the global routing information database trust source integrating multi-dimensional information and developed the function of the protocol level based real-time monitoring system of Internet routing security events. Through these means, it realizes the second-level online monitoring capability of large-scale IP network Internet service routing events, forms the minute-level route leakage interception and route hijacking blocking solutions, and achieves intelligent protection capability of Internet routing security.

Payment is an essential part of e-commerce. Merchants usually rely on third-parties, so-called payment processors, who take care of transferring the payment from the customer to the merchant. How a payment processor interacts with the customer and the merchant varies a lot. Each payment processor typically invents its own protocol that has to be integrated into the merchant’s application and provides the user with a new, potentially unknown and confusing user experience.Pushed by major companies, including Apple, Google, Master-card, and Visa, the W3C is currently developing a new set of standards to unify the online checkout process and “streamline the user’s payment experience”. The main idea is to integrate payment as a native functionality into web browsers, referred to as the Web Payment APIs. While this new checkout process will indeed be simple and convenient from an end-user perspective, the technical realization requires rather significant changes to browsers.Many major browsers, such as Chrome, Firefox, Edge, Safari, and Opera, already implement these new standards, and many payment processors, such as Google Pay, Apple Pay, or Stripe, support the use of Web Payment APIs for payments. The ecosystem is constantly growing, meaning that the Web Payment APIs will likely be used by millions of people worldwide.So far, there has been no in-depth security analysis of these new standards. In this paper, we present the first such analysis of the Web Payment APIs standards, a rigorous formal analysis. It is based on the Web Infrastructure Model (WIM), the most comprehensive model of the web infrastructure to date, which, among others, we extend to integrate the new payment functionality into the generic browser model.Our analysis reveals two new critical vulnerabilities that allow a malicious merchant to over-charge an unsuspecting customer. We have verified our attacks using the Chrome implementation and reported these problems to the W3C as well as the Chrome developers, who have acknowledged these problems. Moreover, we propose fixes to the standard, which by now have been adopted by the W3C and Chrome, and prove that the fixed Web Payment APIs indeed satisfy strong security properties.

Cloud data integrity verification was an important means to ensure data security. We used public key infrastructure (PKI) to manage user keys in Traditional way, but there were problems of certificate verification and high cost of key management. In this paper, RSA signature was used to construct a new identity-based cloud audit protocol, which solved the previous problems caused by PKI and supported forward security, and reduced the loss caused by key exposure. Through security analysis, the design scheme could effectively resist forgery attack and support forward security.

As the COVID-19 continues to spread globally, more and more companies are transforming into remote online offices, leading to the expansion of electronic signatures. However, the existing electronic signatures platform has the problem of data-centered management. The system is subject to data loss, tampering, and leakage when an attack from outside or inside occurs. In response to the above problems, this paper designs an electronic signature solution and implements a prototype system based on the consortium blockchain. The solution divides the contract signing process into four states: contract upload, initiation signing, verification signing, and confirm signing. The signing process is mapped with the blockchain-linked data. Users initiate the signature transaction by signing the uploaded contract's hash. The sign state transition is triggered when the transaction is uploaded to the blockchain under the consensus mechanism and the smart contract control, which effectively ensures the integrity of the electronic contract and the non-repudiation of the electronic signature. Finally, the blockchain performance test shows that the system can be applied to the business scenario of contract signing.

The secure Internet of Things (loT) increasingly relies on digital cryptographic signatures which require a private signature and public verification key. By their intrinsic nature, public keys are meant to be accessible to any interested party willing to verify a given signature. Thus, the storing of such keys is of great concern, since an adversary shall not be able to tamper with the public keys, e.g., on a local filesystem. Commonly used public-key infrastructures (PKIs), which handle the key distribution and storage, are not feasible in most use-cases, due to their resource intensity and high complexity. Thus, the general storing of the public verification keys is of notable interest for low-resource loT networks. By using the Distributed Ledger Technology (DLT), this paper proposes a decentralized concept for storing public signature verification keys in a tamper-resistant, secure, and resilient manner. By combining lightweight public-key exchange protocols with the proposed approach, the storing of verification keys becomes scalable and especially suitable for low-resource loT devices. This paper provides a Proof-of-Concept implementation of the DLT public-key store by extending our previously proposed NFC-Key Exchange (NFC-KE) protocol with a decentralized Hyperledger Fabric public-key store. The provided performance analysis shows that by using the decentralized keystore, the NFC- KE protocol gains an increased tamper resistance and overall system resilience while also showing expected performance degradations with a low real-world impact.

Kerberos protocol is a derivative type of server used for the authentication purpose. Kerberos is a network-based authentication protocol which communicates the tickets from one network to another in a secured manner. Kerberos protocol encrypts the messages and provides mutual authentication. Kerberos uses the symmetric cryptography which uses the public key to strengthen the data confidentiality. The KDS Key Distribution System gives the center of securing the messages. Kerberos has certain disadvantages as it provides public key at both ends. In this proposed approach, the Kerberos are secured by using the HMAC Hash-based Message Authentication Code which is used for the authentication of message for integrity and authentication purpose. It verifies the data by authentication, verifies the e-mail address and message integrity. The computer network and security are authenticated by verifying the user or client. These messages which are transmitted and delivered have to be integrated by authenticating it. Kerberos authentication is used for the verification of a host or user. Authentication is based on the tickets on credentials in a secured way. Kerberos gives faster authentication and uses the unique ticketing system. It supports the authentication delegation with faster efficiency. These encrypt the standard by encrypting the tickets to pass the information.

User authentication based on muscle tension manifested during password typing seems to be an interesting additional layer of security. It represents another way of verifying a person’s identity, for example in the context of continuous verification. In order to explore the possibilities of such authentication method, it was necessary to create a capturing software that records and stores data from EMG (electromyography) sensors, enabling a subsequent analysis of the recorded data to verify the relevance of the method. The work presented here is devoted to the design, implementation and evaluation of such a solution. The solution consists of a protocol and a software application for collecting multimodal data when typing on a keyboard. Myo armbands on both forearms are used to capture EMG and inertial data while additional modalities are collected from a keyboard and a camera. The user experience evaluation of the solution is presented, too.

In recent years, research has focused on exploiting the inherent physical (PHY) characteristics of wireless channels to discriminate between different spatially separated network terminals, mitigating the significant costs of signature-based techniques. In this paper, the legitimacy of the corresponding terminal is firstly verified at the protocol stack’s upper layers, and then the re-authentication process is performed at the PHY-layer. In the latter, a unique PHY-layer signature is created for each transmission based on the spatially and temporally correlated channel attributes within the coherence time interval. As part of the verification process, the PHY-layer signature can be used as a message authentication code to prove the packet’s authenticity. Extensive simulation has shown the capability of the proposed scheme to support high detection probability at small signal-to-noise ratios. In addition, security evaluation is conducted against passive and active attacks. Computation and communication comparisons are performed to demonstrate that the proposed scheme provides superior performance compared to conventional cryptographic approaches.