Biblio

Advancement in network technology provides an opportunity for e-commerce industries to sell digital content. However, multimedia content has the drawback of easy copy and redistribution, which causes rampant piracy. Digital rights management (DRM) systems are developed to address content piracy. Basically, DRM focuses to control content consumption and distribution. In general, to provide copyright protection, DRM system loses flexibility and creates a severe threat to users’ privacy. Moreover, traditional DRM systems are client-server architecture, which cannot handle strategies geographically. These disadvantages discourage the adoption of DRM systems. At the same time, multi-distributor DRM (MD-DRM) system provides a way to facilitate content distribution more effectively. Most of the existing multi-distributor DRM systems are privacy encroaching and do not discuss the useful content distribution framework. To overcome the drawbacks of existing schemes, we propose a privacy-preserving MD-DRM system, which is flexible enough to support location-based content distribution. The proposed scheme maintains a flexible and transparent content distribution without breaching consumer privacy. Besides, the proposed scheme does not violate accountability parameters. This mechanism makes traitor identification possible without violating the privacy rights of authorized consumers.

Vehicular Ad Hoc Network (VANET) is a pervasive network, where vehicles communicate with nearby vehicles and infrastructure nodes, such as Road-side unit (RSU). Information sharing among vehicles is an essential component of an intelligent transportation system (ITS), but security and privacy concerns must be taken into consideration. Security of the network can be improved by granting access only to authenticated vehicles and restricting or revoking access for vehicles involved in misbehavior. In this paper, we present a novel blockchain based approach to authenticate vehicles and notify other vehicles about any unauthorized messages in real time. This helps protect other vehicles in the network from making critical decisions based on false or inaccurate information. In the proposed architecture, vehicles communicate with each other using pseudonyms or pseudo IDs and the Blockchain is used to securely maintain the real identity of all vehicles, which can be linked to the pseudo IDs if needed. The goal is to protect privacy or individual vehicles, while still ensuring accountability in case of misbehavior. The performance of the proposed approach is evaluated for different vehicle and attacker densities, and results demonstrate it has lower authentication delay and communication overhead compared to existing approaches.

The transportation sector is undergoing rapid changes to reduce pollution and increase life quality in urban areas. One of the most effective approaches is flexible car rental and sharing to reduce traffic congestion and parking space issues. In this paper, we envision a flexible car sharing framework where vehicle owners want to make their vehicles available for flexible rental to other users. The owners delegate the management of their vehicles to intermediate services under certain policies, such as municipalities or authorized services, which manage the due infrastructure and services that can be accessed by users. We investigate the design of an accountable solution that allow vehicles owners, who want to share their vehicles securely under certain usage policies, to control that delegated services and users comply with the policies. While monitoring users behavior, our approach also takes care of users privacy, preventing tracking or profiling procedures by other parties. Existing approaches put high trust assumptions on users and third parties, do not consider users' privacy requirements, or have limitations in terms of flexibility or applicability. We propose an accountable protocol that extends standard delegated authorizations and integrate it with Security Credential Management Systems (SCMS), while considering the requirements and constraints of vehicular networks. We show that the proposed approach represents a practical approach to guarantee accountability in realistic scenarios with acceptable overhead.

Recently, vehicular communications have been the focus of industry, research and development fields. There are many benefits of vehicular communications. It improves traffic management and put derivers in better control of their vehicles. Privacy and security protection are collective accountability in which all parties need to actively engage and collaborate to afford safe and secure communication environments. The primary objective of this paper is to exploit the RSS characteristic of physical layer, in order to generate a secret key that can securely be exchanged between legitimated communication vehicles. In this paper, secret key extraction from wireless channel will be the main focus of the countermeasures against VANET security attacks. The technique produces a high rate of bits stream while drop less amount of information. Information reconciliation is then used to remove dissimilarity of two initially extracted keys, to increase the uncertainty associated to the extracted bits. Five values are defined as quantization thresholds for the captured probes. These values are derived statistically, adaptively and randomly according to the readings obtained from the received signal strength.

With the advancement of VLSI technology, Tiled Chip Multicore Processors (TCMP) with packet switched Network-on-Chip (NoC) have been emerged as the backbone of the modern data intensive parallel systems. Due to tight time-to-market constraints, manufacturers are exploring the possibility of integrating several third-party Intellectual Property (IP) cores in their TCMP designs. Presence of malicious Hardware Trojan (HT) in the NoC routers can adversely affect communication between tiles leading to degradation of overall system performance. In this paper, we model an HT mounted on the input buffers of NoC routers that can alter the destination address field of selected NoC packets. We study the impact of such HTs and analyse its first and second order impacts at the core level, cache level, and NoC level both quantitatively and qualitatively. Our experimental study shows that the proposed HT can bring application to a complete halt by stalling instruction issue and can significantly impact the miss penalty of L1 caches. The impact of re-transmission techniques in the context of HT impacted packets getting discarded is also studied. We also expose the unrealistic assumptions and unacceptable latency overheads of existing mitigation techniques for packet header attacks and emphasise the need for alternative cost effective HT management techniques for the same.

High-assurance cryptography leverages methods from program verification and cryptography engineering to deliver efficient cryptographic software with machine-checked proofs of memory safety, functional correctness, provable security, and absence of timing leaks. Traditionally, these guarantees are established under a sequential execution semantics. However, this semantics is not aligned with the behavior of modern processors that make use of speculative execution to improve performance. This mismatch, combined with the high-profile Spectre-style attacks that exploit speculative execution, naturally casts doubts on the robustness of high-assurance cryptography guarantees. In this paper, we dispel these doubts by showing that the benefits of high-assurance cryptography extend to speculative execution, costing only a modest performance overhead. We build atop the Jasmin verification framework an end-to-end approach for proving properties of cryptographic software under speculative execution, and validate our approach experimentally with efficient, functionally correct assembly implementations of ChaCha20 and Poly1305, which are secure against both traditional timing and speculative execution attacks.

In order to protect user privacy and provide better access control in Internet of Things (IoT) environments, designing an appropriate two-party authentication and key exchange protocol is a prominent challenge. In this paper, we propose a lightweight certificateless non-interactive authentication and key exchange (CNAKE) protocol for mutual authentication between remote users and smart devices. Based on elliptic curves, our lightweight protocol provides high security performance, realizes non-interactive authentication between the two entities, and effectively reduces communication overhead. Under the random oracle model, the proposed protocol is provably secure based on the Computational Diffie-Hellman and Bilinear Diffie-Hellman hardness assumption. Finally, through a series of experiments and comprehensive performance analysis, we demonstrate that our scheme is fast and secure.

Modern digital signature schemes can provide more guarantees than the standard notion of (strong) unforgeability, such as offering security even in the presence of maliciously generated keys, or requiring to know a message to produce a signature for it. The use of signature schemes that lack these properties has previously enabled attacks on real-world protocols. In this work we revisit several of these notions beyond unforgeability, establish relations among them, provide the first formal definition of non re-signability, and a transformation that can provide these properties for a given signature scheme in a provable and efficient way.Our results are not only relevant for established schemes: for example, the ongoing NIST PQC competition towards standardizing post-quantum signature schemes has six finalists in its third round. We perform an in-depth analysis of the candidates with respect to their security properties beyond unforgeability. We show that many of them do not yet offer these stronger guarantees, which implies that the security guarantees of these post-quantum schemes are not strictly stronger than, but instead incomparable to, classical signature schemes. We show how applying our transformation would efficiently solve this, paving the way for the standardized schemes to provide these additional guarantees and thereby making them harder to misuse.

A standard requirement for a signature scheme is that it is existentially unforgeable under chosen message attacks (EUF-CMA), alongside other properties of interest such as strong unforgeability (SUF-CMA), and resilience against key substitution attacks.Remarkably, no detailed proofs have ever been given for these security properties for EdDSA, and in particular its Ed25519 instantiations. Ed25519 is one of the most efficient and widely used signature schemes, and different instantiations of Ed25519 are used in protocols such as TLS 1.3, SSH, Tor, ZCash, and WhatsApp/Signal. The differences between these instantiations are subtle, and only supported by informal arguments, with many works assuming results can be directly transferred from Schnorr signatures. Similarly, several proofs of protocol security simply assume that Ed25519 satisfies properties such as EUF-CMA or SUF-CMA.In this work we provide the first detailed analysis and security proofs of Ed25519 signature schemes. While the design of the schemes follows the well-established Fiat-Shamir paradigm, which should guarantee existential unforgeability, there are many side cases and encoding details that complicate the proofs, and all other security properties needed to be proven independently.Our work provides scientific rationale for choosing among several Ed25519 variants and understanding their properties, fills a much needed proof gap in modern protocol proofs that use these signatures, and supports further standardisation efforts.

The performance prediction of user equipment (UE) metrics has many applications in the 5G era and beyond. For instance, throughput prediction can improve carrier selection, adaptive video streaming's quality of experience (QoE), and traffic latency. Many studies suggest distributed learning algorithms (e.g., federated learning (FL)) for this purpose. However, in a multi-tier design, features are measured in different tiers, e.g., UE tier, and gNodeB (gNB) tier. On one hand, neglecting the measurements in one tier results in inaccurate predictions. On the other hand, transmitting the data from one tier to another improves the prediction performance at the expense of increasing network overhead and privacy risks. In this paper, we propose cascaded FL to enhance UE throughput prediction with minimum network footprint and privacy ramifications (if any). The idea is to introduce feedback to conventional FL, in multi-tier architectures. Although we use cascaded FL for UE prediction tasks, the idea is rather general and can be used for many prediction problems in multi-tier architectures, such as cellular networks. We evaluate the performance of cascaded FL by detailed and 3GPP compliant simulations of London's city center. Our simulations show that the proposed cascaded FL can achieve up to 54% improvement over conventional FL in the normalized gain, at the cost of 1.8 MB (without quantization) and no cost with quantization.

Campus Companies and network operators perform risk assessment to inform policy-making, guide infrastructure investments or to comply with security standards such as ISO 27001. Due to the size and complexity of these networks, risk assessment techniques such as attack graphs or trees describe the attacker with a finite set of rules. This characterization of the attacker can easily miss attack vectors or overstate them, potentially leading to incorrect risk estimation. In this work, we propose the first methodology to justify a rule-based attacker model. Conceptually, we add another layer of abstraction on top of the symbolic model of cryptography, which reasons about protocols and abstracts cryptographic primitives. This new layer reasons about Internet-scale networks and abstracts protocols.We show, in general, how the soundness and completeness of a rule-based model can be ensured by verifying trace properties, linking soundness to safety properties and completeness to liveness properties. We then demonstrate the approach for a recently proposed threat model that quantifies the confidentiality of email communication on the Internet, including DNS, DNSSEC, and SMTP. Using off-the-shelf protocol verification tools, we discover two flaws in their threat model. After fixing them, we show that it provides symbolic soundness.

The advent of 5G, one of the most recent and promising technologies currently under deployment, fulfills the emerging needs of mobile subscribers by introducing several new technological advancements. However, this may lead to numerous attacks in the emerging 5G networks. Thus, to guarantee the secure transmission of user data, 5G Authentication protocols such as Extensible Authentication Protocol - Authenticated Key Agreement Protocol (EAP-AKA) were developed. These protocols play an important role in ensuring security to the users as well as their data. However, there exists no guarantees about the security of the protocols. Thus formal verification is necessary to ensure that the authentication protocols are devoid of vulnerabilities or security loopholes. Towards this goal, we formally verify the security of the 5G EAP-AKA protocol using an automated verification tool called ProVerif. ProVerif identifies traces of attacks and checks for security loopholes that can be accessed by the attackers. In addition, we model the complete architecture of the 5G EAP-AKA protocol using the language called typed pi-calculus and analyze the protocol architecture through symbolic model checking. Our analysis shows that some cryptographic parameters in the architecture can be accessed by the attackers which cause the corresponding security properties to be violated.

Today's Internet is built on decades-old networking protocols that lack scalability, reliability, and security. In response, the networking community has developed path-aware Internet architectures that solve these issues while simultaneously empowering end hosts. In these architectures, autonomous systems construct authenticated forwarding paths based on their routing policies. Each end host then selects one of these authorized paths and includes it in the packet header, thus allowing routers to efficiently determine how to forward the packet. A central security property of these architectures is path authorization, requiring that packets can only travel along authorized paths. This property protects the routing policies of autonomous systems from malicious senders.The fundamental role of packet forwarding in the Internet and the complexity of the authentication mechanisms employed call for a formal analysis. In this vein, we develop in Isabelle/HOL a parameterized verification framework for path-aware data plane protocols. We first formulate an abstract model without an attacker for which we prove path authorization. We then refine this model by introducing an attacker and by protecting authorized paths using (generic) cryptographic validation fields. This model is parameterized by the protocol's authentication mechanism and assumes five simple verification conditions that are sufficient to prove the refinement of the abstract model. We validate our framework by instantiating it with several concrete protocols from the literature and proving that they each satisfy the verification conditions and hence path authorization. No invariants must be proven for the instantiation. Our framework thus supports low-effort security proofs for data plane protocols. The results hold for arbitrary network topologies and sets of authorized paths, a guarantee that state-of-the-art automated security protocol verifiers cannot currently provide.

Controller area network is the serial communication protocol, which broadcasts the message on the CAN bus. The transmitted message is read by all the nodes which shares the CAN bus. The message can be eavesdropped and can be re-used by some other node by changing the information or send it by duplicate times. The message reused after some delay is replay attack. In this paper, the CAN network with three CAN nodes is implemented using the universal verification components and the replay attack is demonstrated by creating the faulty node. Two types of replay attack are implemented in this paper, one is to replay the entire message and the other one is to replay only the part of the frame. The faulty node uses the first replay attack method where it behaves like the other node in the network by duplicating the identifier. CAN frame except the identifier is reused in the second method which is hard to detect the attack as the faulty node uses its own identifier and duplicates only the data in the CAN frame.

Mobile payment protocols have attracted widespread attention over the past decade, due to advancements in digital technology. The use of these protocols in online industries can dramatically improve the quality of online services. However, the central issue of concern when utilizing these types of systems is their accountability, which ensures trust between the parties involved in payment transactions. It is, therefore, vital for researchers to investigate how to handle the accountability of mobile payment protocols. In this research, we introduce a secure mobile payment protocol to overcome this problem. Our payment protocol combines all the necessary security features, such as confidentiality, integrity, authentication, and authorization that are required to build trust among parties. In other words, is the properties of mutual authentication and non-repudiation are ensured, thus providing accountability. Our approach can resolve any conflicts that may arise in payment transactions between parties. To prove that the proposed protocol is correct and complete, we use the Scyther and AVISPA tools to verify our approach formally.

UPI (Unified Payments Interface) is a framework in India wherein customers can send payments to merchants from their smartphones. The framework consists of UPI servers that are connected to the banks at the sender and receiver ends. To send and receive payments, customers and merchants would have to first register themselves with UPI servers by executing a registration protocol using payment apps such as BHIM, PayTm, Google Pay, and PhonePe. Weaknesses were recently reported on these protocols that allow attackers to make money transfers on behalf of innocent customers and even empty their bank accounts. But the reported weaknesses were found after informal and manual analysis. However, as history has shown, formal analysis of cryptographic protocols often reveals flaws that could not be discovered with manual inspection. In this paper, we model UPI protocols in the pattern of traditional cryptographic protocols such that they can be rigorously studied and analyzed using formal methods. The modeling simplifies many of the complexities in the protocols, making it suitable to analyze and verify UPI protocols with popular analysis and verification tools such as the Constraint Solver, ProVerif and Tamarin. Our modeling could also be used as a general framework to analyze and verify many other financial payment protocols than just UPI protocols, giving it a broader applicability.

In the era of big data and artificial intelligence, computer networks have become an important infrastructure, and the Internet has become ubiquitous. The most basic property of computer networks is reachability. The needs of the modern Internet mainly include cost, performance, reliability, and security. However, even for experienced network engineers, it is very difficult to manually conFigure the network to meet the needs of the modern large-scale Internet. The engineers often make mistakes, which can cause network paralysis, resulting in incalculable losses. Due to the development of automatic reasoning technology, automatic verification of network configuration is used to avoid mistakes. Network verification is at least an NP-C problem, so it is necessary to compress the network to reduce the network scale, thereby reducing the network verification time. This paper proposes a new model of network modeling, which is more suitable for the verification of network configuration on common protocols (such as RIP, BGP). On the basis of the existing compression method, two compression rules are added to compress the modeled network, reducing network verification time and conducting network reachability verification experiments on common networks. The experimental results are slightly better than the current compression methods.

This paper deals with a problem that arises in vertical composition of protocols, i.e., when a channel protocol is used to encrypt and transport arbitrary data from an application protocol that uses the channel. Our work proves that we can verify that the channel protocol ensures its security goals independent of a particular application. More in detail, we build a general paradigm to express vertical composition of an application protocol and a channel protocol, and we give a transformation of the channel protocol where the application payload messages are replaced by abstract constants in a particular way that is feasible for standard automated verification tools. We prove that this transformation is sound for a large class of channel and application protocols. The requirements that channel and application have to satisfy for the vertical composition are all of an easy-to-check syntactic nature.

Given the central importance of designing secure protocols, providing solid mathematical foundations and computer-assisted methods to attest for their correctness is becoming crucial. Here, we elaborate on the formal approach introduced by Bana and Comon in [10], [11], which was originally designed to analyze protocols for a fixed number of sessions, and lacks support for proof mechanization.In this paper, we present a framework and an interactive prover allowing to mechanize proofs of security protocols for an arbitrary number of sessions in the computational model. More specifically, we develop a meta-logic as well as a proof system for deriving security properties. Proofs in our system only deal with high-level, symbolic representations of protocol executions, similar to proofs in the symbolic model, but providing security guarantees at the computational level. We have implemented our approach within a new interactive prover, the Squirrel prover, taking as input protocols specified in the applied pi-calculus, and we have performed a number of case studies covering a variety of primitives (hashes, encryption, signatures, Diffie-Hellman exponentiation) and security properties (authentication, strong secrecy, unlinkability).

In protocol verification we observe a wide spectrum from fully automated methods to interactive theorem proving with proof assistants like Isabelle/HOL. The latter provide overwhelmingly high assurance of the correctness, which automated methods often cannot: due to their complexity, bugs in such automated verification tools are likely and thus the risk of erroneously verifying a flawed protocol is non-negligible. There are a few works that try to combine advantages from both ends of the spectrum: a high degree of automation and assurance. We present here a first step towards achieving this for a more challenging class of protocols, namely those that work with a mutable long-term state. To our knowledge this is the first approach that achieves fully automated verification of stateful protocols in an LCF-style theorem prover. The approach also includes a simple user-friendly transaction-based protocol specification language embedded into Isabelle, and can also leverage a number of existing results such as soundness of a typed model

Demand-side management (DSM) plays a significant function in the smart distribution system to make informed decisions from both the consumer and supplier side with regards to energy consumption to redesign the load profile and to decrease the peak load demand. This study extensively reviews the demand-side management (DSM) strategies along with both demand response and energy efficiency policies. The major objective of this paper is to enumerate the relevant features responsible to strengthen the DSM effectively, particularly for residential energy demand and the limits to energy indicators. Secondly, the large untapped and hidden potential and the associated barriers to energy efficiency enhancement are focused and surveyed for formulating a better number of potential policy responses. This further explores the portfolio approach with bundled strategies to reflect on the power market through enhancing the strength of individual residential measures through complementary policies to reduce the weaknesses. This concludes at last with the findings of possible holistic measures related to various approaches and attributes findings that reinforce the DSM strategies to enhance energy management and cost-effectiveness. Apart from that the architecture, formulation of optimization problems, and various approaches are presented to help the readers to develop research in this direction to maximize the total system peak demand, overall load factor, and utility revenue with the minimized customer electric bill.

In recent years, the commodities industry has grown rapidly under the stimulus of domestic demand and the expansion of cross-border trade. It has also been combined with the rapid development of e-commerce technology in the same period to form a flexible and efficient e-commerce system for bulk commodities. However, the hasty combination of both has inspired a lack of effective regulatory measures in the bulk industry, leading to constant industry chaos. Among them, the problem of lagging evidence in regulatory platforms is particularly prominent. Based on this, we design a blockchain-based evidential and secure bulk-commodity supervisory system (abbr. BeBus). Setting different privacy protection policies for each participant in the system, the solution ensures effective forensics and tamper-proof evidence to meet the needs of the bulk business scenario.

Telecommunications and data are pervasive in almost each aspect of our every-day life and new concerns progressively arise as a result of stakes related to privacy and data protection [1]. Indeed, systems development becomes data-centric leading to an ecosystem where a variety of players intervene (citizens, industry, regulators) and where the policies regarding data usage and utilization are far from consensual. The new General Data Protection Regulation (GDPR) enacted by the European Commission in 2018 has introduced new provisions including principles for lawfulness, fairness, transparency, etc. thus endorsing data subjects with new rights in regards to their personal data. In this context, a growing need for approaches that conceptualize and help engineers to integrate GDPR and privacy provisions at design time becomes paramount. This paper presents a comprehensive approach to support different phases of the design process with special attention to the integration of privacy and data protection principles. Among others, it is a generic model-based approach that can be specialized according to the specifics of different application domains.

We perform the first post EU General Data Protection Regulation (GDPR) usability study of privacy policies for mobile apps. For our analysis, we collect a dataset of historical (prior to GDPR implementation in May 2018) and contemporary privacy policies in different categories. In contrast to the common belief, that after the GDPR most of the privacy policies are easier to understand, our analysis shows that this is not so.

The COVID-19 pandemic has recently emerged as a worldwide health emergency that necessitates coordinated international measures. To contain the virus's spread, governments and health organisations raced to develop vaccines that would lower Covid-19 morbidity, relieve pressure on healthcare systems, and allow economies to open. Following the COVID-19 vaccine, the vaccination certificate has been adopted to help the authorities formulate policies by controlling cross-border travelling. To address serious privacy concerns and eliminate the need for third parties to retain the trust and govern user data, in this paper, we leverage blockchain technologies in developing a secure and verifiable vaccination certificate. Our approach has the advantage of utilising a hybrid approach that implements different advanced technologies, such as the self-sovereignty concept, smart contracts and interPlanetary File System (IPFS). We rely on verifiable credentials paired with smart contracts to make decisions about who can access the system and provide on-chain verification and validation of the user and issuer DIDs. The approach was further analysed, with a focus on performance and security. Our analysis shows that our solution satisfies the security requirements for immunisation certificates.