Biblio

Until recently, IT security received limited attention within the scope of Process Control Systems (PCS). In the past, PCS consisted of isolated, specialized components running closed process control applications, where hardware was placed in physically secured locations and connections to remote network infrastructures were forbidden. Nowadays, industrial communications are fully exploiting the plethora of features and novel capabilities deriving from the adoption of commodity off the shelf (COTS) hardware and software. Nonetheless, the reliance on COTS for remote monitoring, configuration and maintenance also exposed PCS to significant cyber threats. In light of these issues, this paper presents the steps for the design, verification and implementation of a lightweight remote attestation protocol. The protocol is aimed at providing a secure software integrity verification scheme that can be readily integrated into existing industrial applications. The main novelty of the designed protocol is that it encapsulates key elements for the protection of both participating parties (i.e., verifier and prover) against cyber attacks. The protocol is formally verified for correctness with the help of the Scyther model checking tool. The protocol implementation and experimental results are provided for a Phoenix-Contact industrial controller, which is widely used in the automation of gas transportation networks in Romania.

We propose a real time authentication scheme for smart grids which improves upon existing schemes. Our scheme is useful in many situations in smart grid operations. The smart grid Control Center (CC) communicates with the sensor nodes installed in the transmission lines so as to utilize real time data for monitoring environmental conditions in order to determine optimum power transmission capacity. Again a smart grid Operation Center (OC) communicates with several Residential Area (RA) gateways (GW) that are in turn connected to the smart meters installed in the consumer premises so as to dynamically control the power supply to meet demand based on real time electricity use information. It is not only necessary to authenticate sensor nodes and other smart devices, but also protect the integrity of messages being communicated. Our scheme is based on batch signatures and are more efficient than existing schemes. Furthermore our scheme is based on stronger notion of security, whereby the batch of signatures verify only if all individual signatures are valid. The communication overhead is kept low by using short signatures for verification.

Deploying Internet of Things (IoT) applications over wireless networks has become commonplace. The transmission of unencrypted data between IOT devices gives malicious users the opportunity to steal personal information. Despite resource-constrained in the IoT environment, devices need to apply authentication methods to encrypt information and control access rights. This paper introduces a trusted third-party method of identity verification and exchange of keys that minimizes the resources required for communication between devices. A device must be registered in order to obtain a certificate and a session key, for verified identity and encryption communication. Malicious users will not be able to obtain private information or to use it wrongly, as this would be protected by authentication and access control

We present Minesweeper, a tool to verify that a network satisfies a wide range of intended properties such as reachability or isolation among nodes, waypointing, black holes, bounded path length, load-balancing, functional equivalence of two routers, and fault-tolerance. Minesweeper translates network configuration files into a logical formula that captures the stable states to which the network forwarding will converge as a result of interactions between routing protocols such as OSPF, BGP and static routes. It then combines the formula with constraints that describe the intended property. If the combined formula is satisfiable, there exists a stable state of the network in which the property does not hold. Otherwise, no stable state (if any) violates the property. We used Minesweeper to check four properties of 152 real networks from a large cloud provider. We found 120 violations, some of which are potentially serious security vulnerabilities. We also evaluated Minesweeper on synthetic benchmarks, and found that it can verify rich properties for networks with hundreds of routers in under five minutes. This performance is due to a suite of model-slicing and hoisting optimizations that we developed, which reduce runtime by over 460x for large networks.

We consider the problem of verifying the security of finitely many sessions of a protocol that tosses coins in addition to standard cryptographic primitives against a Dolev-Yao adversary. Two properties are investigated here - secrecy, which asks if no adversary interacting with a protocol P can determine a secret sec with probability textgreater 1 - p; and indistinguishability, which asks if the probability observing any sequence 0$øverline$ in P1 is the same as that of observing 0$øverline$ in P2, under the same adversary. Both secrecy and indistinguishability are known to be coNP-complete for non-randomized protocols. In contrast, we show that, for randomized protocols, secrecy and indistinguishability are both decidable in coNEXPTIME. We also prove a matching lower bound for the secrecy problem by reducing the non-satisfiability problem of monadic first order logic without equality.

The IoT node works mostly in a specific scenario, and executes the fixed program. In order to make it suitable for more scenarios, this paper introduces a kind of the IoT node, which can change program at any time. And this node has intelligent and dynamic reconfigurable features. Then, a transport protocol is proposed. It enables this node to work in different scenarios and perform corresponding program. Finally, we use Verilog to design and FPGA to verify. The result shows that this protocol is feasible. It also offers a novel way of the IoT.

Population protocols are a well established model of computation by anonymous, identical finite state agents. A protocol is well-specified if from every initial configuration, all fair executions of the protocol reach a common consensus. The central verification question for population protocols is the well-specification problem: deciding if a given protocol is well-specified. Esparza et al. have recently shown that this problem is decidable, but with very high complexity: it is at least as hard as the Petri net reachability problem, which is EXPSPACE-hard, and for which only algorithms of non-primitive recursive complexity are currently known. In this paper we introduce the class WS3 of well-specified strongly-silent protocols and we prove that it is suitable for automatic verification. More precisely, we show that WS3 has the same computational power as general well-specified protocols, and captures standard protocols from the literature. Moreover, we show that the membership problem for WS3 reduces to solving boolean combinations of linear constraints over N. This allowed us to develop the first software able to automatically prove well-specification for all of the infinitely many possible inputs.

The proliferation of connected devices has motivated a surge in the development of cryptographic protocols to support a diversity of devices and use cases. To address this trend, we propose continuous verification, a methodology for secure cryptographic protocol design that consists of three principles: (1) repeated use of verification tools; (2) judicious use of common message components; and (3) inclusion of verifiable model specifications in standards. Our recommendations are derived from previous work in the formal methods community, as well as from our past experiences applying verification tools to improve standards. Through a case study of IETF protocols for the IoT, we illustrate the power of continuous verification by (i) discovering flaws in the protocols using the Cryptographic Protocol Shapes Analyzer (CPSA); (ii) identifying the corresponding fixes based on the feedback provided by CPSA; and (iii) demonstrating that verifiable models can be intuitive, concise and suitable for inclusion in standards to enable third-party verification and future modifications.

Thumbnail preserving encryption (TPE) was suggested by Wright et al. [Information Hiding & Multimedia Security Workshop 2015] as a way to balance privacy and usability for online image sharing. The idea is to encrypt a plaintext image into a ciphertext image that has roughly the same thumbnail as well as retaining the original image format. At the same time, TPE allows users to take advantage of much of the functionality of online photo management tools, while still providing some level of privacy against the service provider. In this work we present two new approximate TPE encryption schemes. In our schemes, ciphertexts and plaintexts have perceptually similar, but not identical, thumbnails. Our constructions are the first TPE schemes designed to work well with JPEG compression. In addition, we show that they also have provable security guarantees that characterize precisely what information about the plaintext is leaked by the ciphertext image. We empirically evaluate our schemes according to the similarity of plaintext & ciphertext thumbnails, increase in file size under JPEG compression, preservation of perceptual image hashes, among other aspects. We also show how approximate TPE can be an effective tool to thwart inference attacks by machine-learning image classifiers, which have shown to be effective against other image obfuscation techniques.

Deduplication is a widely used technique for reducing storage space of cloud service providers. Yet, it is unclear how to support deduplication of encrypted data securely until the study of Bellareetal on message-locked encryption (Eurocrypt 2013). Since then, there are many improvements such as strengthening its security, reducing client storage, etc. While updating a (shared) file is common, there is little attention on how to efficiently update large encrypted files in a remote storage with deduplication. To modify even a single bit, existing solutions require the trivial and expensive way of downloading and decrypting the large ciphertext. We initiate the study of updatable block-level message-locked encryption. We propose a provably secure construction that is efficiently updatable with O(logtextbarFtextbar) computational cost, where textbarFtextbar is the file size. It also supports proof-of-ownership, a nice feature which protects storage providers from being abused as a free content distribution network.

Encrypted databases, a popular approach to protecting data from compromised database management systems (DBMS's), use abstract threat models that capture neither realistic databases, nor realistic attack scenarios. In particular, the "snapshot attacker" model used to support the security claims for many encrypted databases does not reflect the information about past queries available in any snapshot attack on an actual DBMS. We demonstrate how this gap between theory and reality causes encrypted databases to fail to achieve their "provable security" guarantees.

For a secure communication over an insecure channel the Diffie-Hellman key exchange protocol (DHKEP) is treated as the de facto standard. However, it suffers form server-side compromisation, identity compromisation, man-in-the-middle, replay attacks, etc. Also, there are single point of vulnerability (SOV), single point of failure (SOF) and user privacy preservation issues. This work proposes an identity-based two-server DHKEP to address the aforesaid issues and alleviating the attacks. To preserve user identity from outside intruders, a k-anonymity based identity hiding principle has been adopted. Further, to ensure efficient utilization of channel bandwidth, the proposed scheme employs elliptic curve cryptography. The security analysis substantiate that our scheme is provably secure and successfully addressed the above-mentioned issues. The performance study contemplates that the overhead of the protocol is reasonable and comparable with other schemes.

A strong designated verifier signature (SDVS) is a variation of traditional digital signatures, since it allows a signer to designate an intended receiver as the verifier rather than anyone. To do this, a signer must incorporate the verifier's public key with the signing procedure such that only the intended receiver could verify this signature with his/her private key. Such a signature further enables a designated verifier to simulate a computationally indistinguishable transcript intended for himself. Consequently, no one can identify the real signer's identity from a candidate signer and a designated verifier, which is referred to as the property of signer ambiguity. A strong notion of signer ambiguity states that no polynomial-time adversary can distinguish the real signer of a given SDVS that is not received by the designated verifier, even if the adversary has obtained the signer's private key. In 2013, Islam and Biswas proposed a provably secure certificateless strong designated verifier signature (CL-SDVS) scheme based on bilinear pairings. In this paper, we will demonstrate that their scheme fails to satisfy strong signer ambiguity and must assume a trusted private key generator (PKG). In other words, their CL-SDVS scheme is vulnerable to both key-compromise and malicious PKG attacks. Additionally, we present an improved variant to eliminate these weaknesses.

We consider the situation, where an adversary may learn the ephemeral values used by the prover within an identification protocol, aiming to get the secret keys of the user, or just to impersonate the prover subsequently. Unfortunately, most classical cryptographic identification protocols are exposed to such attacks, which might be quite realistic in case of software implementations. According to a recent proposal from SECIT-2017, we regard a scheme to be secure, if a malicious verifier, allowed to set the prover's ephemerals in the query stage, cannot impersonate the prover later on. We focus on the Okamoto Identification Scheme (IS), and show how to make it immune to the threats described above. Via reduction to the GDH Problem, we provide security guarantees in case of insufficient control over the unit executing Okamoto identification protocol (the standard Okamoto protocol is insecure in this situation).

In this paper, we propose principles of information control and sharing that support ORCON (ORiginator COntrolled access control) models while simultaneously improving components of confidentiality, availability, and integrity needed to inherently support, when needed, responsibility to share policies, rapid information dissemination, data provenance, and data redaction. This new paradigm of providing unfettered and unimpeded access to information by authorized users, while at the same time, making access by unauthorized users impossible, contrasts with historical approaches to information sharing that have focused on need to know rather than need to (or responsibility to) share.

A one-message unilateral entity authentication scheme allows one party, called the prover, to authenticate himself, i.e., to prove his identity, to another party, called the verifier, by sending a single authentication message. In this paper we consider schemes where the prover and the verifier do not share any secret information, such as a password, in advance. We propose the first theoretical characterization for one-message unilateral entity authentication schemes, by formalizing the security requirements for such schemes with respect to different kinds of adversaries. Afterwards, we propose three provably-secure constructions for one-message unilateral entity authentication schemes.

Various critical state models have been developed to understand the hysteresis loss mechanism of high-temperature superconducting (HTSC) films. The analytic relation between the hysteresis loss and the remanent field was obtained based on Bean's critical state model for thin films in the full-penetration case. Furthermore, numerical calculation of local hysteresis loops was carried out by Kim's critical state model. In this paper, we investigated local hysteresis losses for a GdBCO coated conductor by using low-temperature scanning Hall probe microscopy and reproduced the experimental results by applying the critical state model. Because of the demagnetizing effect in thin films, analysis of local hysteresis losses can be useful approach to understand of total hysteresis losses.

We demonstrate how a unique nanomodulation within a continuous ferromagnetic film can induce magnetic dipoles at predefined, submicrometer scale locations, which can tune the global magnetic properties of the film due to dipole-dipole interactions. Arrays of tunable magnetic dipoles are generated with in-plane and out-of-plane directions, which can be rotated in-plane within the three-dimensional (3-D) modulated structure of a continuous film. In-plane magnetic dipole rotation enables a methodology to control overall magnetic properties of a ferromagnetic thin film. Formation of magnetic dipoles and their tunability were studied in detail by magnetic force microscopy, high-resolution magnetic measurements, and micromagnetic simulation of a nanomodulated Ni45Fe55 alloy film. A pattern larger than a single magnetic domain would normally form a vortex in the remanent state. However, here the unique 3-D nanostructure prevents vortex formation due to the competition between in-plane and out-of-plane dipole-dipole interaction giving rise to a metastable state. Experimentally, at zero remanence, the magnetization goes through a transformation from a metastable to a stable state, where the dipole-dipole interaction depends on their geometrical arrangement. Thus, the magnetic properties of the continuous film can be varied by the proposed pattern geometry. A detail analytical study of the dipolar energy for the system agrees well with the experimental and simulated results.

Having significant role in the storing, delivering and conversion of the energy, the permanent magnets are key elements in the actual technology. In many applications, the gap between ferrites and rare earths (RE) based sintered permanent magnets is nowadays filled by RE bonded magnets, used in more applications, below their magnetic performances. Therewith, the recent trends in the RE market concerning their scarcity, impose EU to consider alternative magnets (without RE) to fill such gap. The paper presents the chemical synthesis of the exchange coupled SrFe12O19/CoFe2O4 nanocomposites, based on nanoferrites. The appropriate annealing leads to the increasing of the main magnetic characteristics, saturation magnetization MS and intrinsic coercivity Hc, in the range of 49 - 53 emu/g, respectively 126.5 - 306 kA/m. The value reached for the ratio between remanent magnetization and saturation magnetization is higher than 0.5, fact that proved that between the two magnetic phases occurred exchange interaction.

Summary form only given. All-optical switching (AOS) has been observed in ferromagnetic (FM) layers and synthetic ferrimagnetic heterostructures [1-4]. In this work, we use anomalous Hall effect (AHE) measurements to demonstrate controlled helicity-dependent switching in synthetic ferrimagnetic heterostructures. The two FM layers are engineered to have different Curie temperatures Tc1 (fixed) and Tc2 (variable). We show that irrespective of whether Tc2 is higher or lower than Tc1, the final magnetic configuration of the heterostructure is controlled by using the laser polarization to set the magnetic state of the FM layer with the highest Tc. All samples were grown on glass substrates at room temperature by DC magnetron sputtering. Two sets of samples were prepared. The first set are single FM layers with layer composition Ta (3 nm)/Pt (4 nm)/FM1(2)/Pt capping (4 nm), where FM1 = Co (0.6 nm) is a Co layer and FM2 = CoFeB (tCoFeB)/Pt(0.4 nm)/ CoFeB (tCoFeB) (0.2 ≤ tCoFeB ≤ 0.6 nm) is a composite CoFeB layer where both CoFeB layers are ferromagnetically coupled and act as a single layer. FM1 and FM2 were used to produce the second set of synthetic ferrimagnetic samples with layer structure Ta (3 nm)/Pt (4 nm)/FM1/Pt (0.4 nm)/Ru (0.9 nm)/Pt (0.4 nm)/FM2/Pt capping (4 nm). The Ru layer provides the antiferromagnetic RKKY interlayer exchange coupling between the adjacent FM1 and FM2 layers while the Pt layers on either side of the Ru layer can tune the strength of the coupling and stabilize their perpendicular anisotropy [5]. To study the AOS, we use a Ti: sapphire fs-laser with a wavelength of 800 nm and a pulse duration of 43 fs. A quarter-wave plate is used to create a circularly polarized [right(σ+) and left-handed (σ-)] beam. We first measured the magnetic properties of the FM1 and FM2 layers using vibrating sample magnetometry (VSM). All FM samples show full remanence in perpendicular hyst- resis loops at room temperature (not shown). The temperature-dependent magnetization scans (not shown) give a Curie temperature Tc1 of 524 K for FM1. For FM2, increasing tCoFeB increases its Curie temperatureTc2. At tCoFeB = 0.5 nm, Tc2 - Tc1. Hall crosses are patterned by optical lithography and ion milling. The width of the current carrying wire is - 5 um, giving a DC current density of - 6 x 109 A/m2 during the measurement. Figure 1(a) shows the resulting perpendicular Hall hysteresis loop of the synthetic ferrimagnetic sample with tCoFeB = 0.2 nm. At remanence, the stable magnetic configurations are the two antiparallel orientations of FM1 and FM2 [State I and II in Fig. 1(a)]. To study the AOS, we swept the laser beam with a power of 0.45 mW and a speed of 1 μm/sec across the Hall cross, and the corresponding Hall voltage was constantly monitored. In Fig. 1(b), we show the normalized Hall voltage, VHall, as a function of the laser beam position x for both beam polarizations σ+ and σ-. The initial magnetic configuration was State I. When the beam is at the center of the cross (position B), both beam polarizations give VHall - 0. As the beam leaves the cross (position C), the σbeam changes the magnetic configurations from State I to State II (FM1 magnetization pointing down), while the system reverts to State I using the σ+ beam. Changing the initial configuration from State I to State II results in the same final magnetic configurations, determined by the laser beam polarizations (not shown). Similar results (not shown) were obtained for samples with tCoFeB ≤ 0.4 nm. However, at tCoFeB = 0.6 nm, the σbeam results in the final magnetic configurations with FM2 magnetization pointing down (State I) and the σ+ beam results in the State II configuration, suggesting that the final state is determined by the beam polar

Alternatives to rare earth permanent magnets, such as alnico, will reduce supply instability, increase sustainability, and could decrease the cost of permanent magnets, especially for high-temperature applications, such as traction drive motors. Alnico magnets with moderate coercivity, high remanence, and relatively high-energy product are conventionally processed by directional solidification and (significant) final machining, contributing to increased costs and additional material waste. Additive manufacturing (AM) is developing as a cost effective method to build net-shape 3-D parts with minimal final machining and properties comparable to wrought parts. This paper describes initial studies of net-shape fabrication of alnico magnets by AM using a laser engineered net shaping (LENS) system. High-pressure gas atomized pre-alloyed powders of two different modified alnico “8” compositions, with high purity and sphericity, were built into cylinders using the LENS process, and followed by heat treatment. The magnetic properties showed improvement over their cast and sintered counterparts. The resulting alnico permanent magnets were characterized using scanning electron microscopy, energy dispersive spectroscopy, electron backscatter diffraction, and hysteresisgraph measurements. These results display the potential for net-shape processing of alnico permanent magnets for use in next generation traction-drive motors and other applications requiring high temperatures and/or complex engineered part geometries.

The heat load of the original cryomodules for the continuous electron beam accelerator facility is 50% higher than the target value of 100 W at 2.07 K for refurbished cavities operating at an accelerating gradient of 12.5 MV/m. This issue is due to the quality factor of the cavities being 50% lower in the cryomodule than when tested in a vertical cryostat, even at low RF field. Previous studies were not conclusive about the origin of the additional losses. We present the results of a systematic study of the additional losses in a five-cell cavity from a decommissioned cryomodule after attaching components, which are part of the cryomodule, such as the cold tuner, the He tank, and the cold magnetic shield, prior to cryogenic testing in a vertical cryostat. Flux-gate magnetometers and temperature sensors are used as diagnostic elements. Different cool-down procedures and tests in different residual magnetic fields were investigated during the study. Three flux-gate magnetometers attached to one of the cavities installed in the refurbished cryomodule C50-12 confirmed the hypothesis of high residual magnetic field as a major cause for the increased RF losses.

In order to investigate the relationship and effect on the performance of magnetic modulator among applied DC current, excitation source, excitation loop current, sensitivity and induced voltage of detecting winding, this paper measured initial permeability, maximum permeability, saturation magnetic induction intensity, remanent magnetic induction intensity, coercivity, saturated magnetic field intensity, magnetization curve, permeability curve and hysteresis loop of main core 1J85 permalloy of magnetic modulator based on ballistic method. On this foundation, employ curve fitting tool of MATLAB; adopt multiple regression method to comprehensively compare and analyze the sum of squares due to error (SSE), coefficient of determination (R-square), degree-of-freedom adjusted coefficient of determination (Adjusted R-square), and root mean squared error (RMSE) of fitting results. Finally, establish B-H curve mathematical model based on the sum of arc-hyperbolic sine function and polynomial.

Ensemble waveform analysis is used to calculate signal to noise ratio (SNR) and other recording characteristics from micromagnetically modeled heat assisted magnetic recording waveforms and waveforms measured at both drive and spin-stand level. Using windowing functions provides the breakdown between transition and remanence SNRs. In addition, channel bit density (CBD) can be extracted from the ensemble waveforms using the di-bit extraction method. Trends in both transition SNR, remanence SNR, and CBD as a function of ambient temperature at constant track width showed good agreement between model and measurement. Both model and drive-level measurement show degradation in SNR at higher ambient temperatures, which may be due to changes in the down-track profile at the track edges compared with track center. CBD as a function of cross-track position is also calculated for both modeling and spin-stand measurements. The CBD widening at high cross-track offset, which is observed at both measurement and model, was directly related to the radius of curvature of the written transitions observed in the model and the thermal profiles used.

A significant advance in magnetic field management in a fully assembled superconducting radiofrequency cryomodule has been achieved and is reported here. Demagnetization of the entire cryomodule after assembly is a crucial step toward the goal of average magnetic flux density less than 0.5 μT at the location of the superconducting radio frequency cavities. An explanation of the physics of demagnetization and experimental results are presented.