Formal modelling and analysis of DNP3 secure authentication

Supervisory Control and Data Acquisition (SCADA) systems are one of the key foundations of smart grids. The Distributed Network Protocol version 3 (DNP3) is a standard SCADA protocol designed to facilitate communications in substations and smart grid nodes. The protocol is embedded with a security mechanism called Secure Authentication (DNP3-SA). This mechanism ensures that end-to-end communication security is provided in substations. This paper presents a formal model for the behavioural analysis of DNP3-SA using Coloured Petri Nets (CPN). Our DNP3-SA CPN model is capable of testing and verifying various attack scenarios: modification, replay and spoofing, combined complex attack and mitigation strategies. Using the model has revealed a previously unidentified flaw in the DNP3-SA protocol that can be exploited by an attacker that has access to the network interconnecting DNP3 devices. An attacker can launch a successful attack on an outstation without possessing the pre-shared keys by replaying a previously authenticated command with arbitrary parameters. We propose an update to the DNP3-SA protocol that removes the flaw and prevents such attacks. The update is validated and verified using our CPN model proving the effectiveness of the model and importance of the formal protocol analysis.

A strong lightweight authentication protocol for low-cost RFID systems

RFID is an important technology that can be used to create the ubiquitous society. But an RFID system uses open radio frequency signal to transfer information and this leads to pose many serious threats to its privacy and security. In general, the computing and storage resources in an RFID tag are very limited and this makes it difficult to solve its secure and private problems, especially for low-cost RFID tags. In order to ensure the security and privacy of low-cost RFID systems we propose a lightweight authentication protocol based on Hash function. This protocol can ensure forward security and prevent information leakage, location tracing, eavesdropping, replay attack and spoofing. This protocol completes the strong authentication of the reader to the tag by twice authenticating and it only transfers part information of the encrypted tag’s identifier for each session so it is difficult for an adversary to intercept the whole identifier of a tag. This protocol is simple and it takes less computing and storage resources, it is very suitable to some low-cost RFID systems.

Graphical method to include temperature variation of activation energy in Hall data analysis

A graphical method is presented for Hall data analysis, including the temperature variation of activation energy due to screening. This method removes the discrepancies noted in the analysis of recently reported Hall data on Si(In).

Double-authentication-preventing signatures

Digital signatures are often used by trusted authorities to make unique bindings between a subject and a digital object; for example, certificate authorities certify a public key belongs to a domain name, and time-stamping authorities certify that a certain piece of information existed at a certain time. Traditional digital signature schemes however impose no uniqueness conditions, so a trusted authority could make multiple certifications for the same subject but different objects, be it intentionally, by accident, or following a (legal or illegal) coercion. We propose the notion of a double-authentication-preventing signature, in which a value to be signed is split into two parts: a subject and a message. If a signer ever signs two different messages for the same subject, enough information is revealed to allow anyone to compute valid signatures on behalf of the signer. This double-signature forgeability property discourages signers from misbehaving—a form of self-enforcement—and would give binding authorities like CAs some cryptographic arguments to resist legal coercion. We give a generic construction using a new type of trapdoor functions with extractability properties, which we show can be instantiated using the group of sign-agnostic quadratic residues modulo a Blum integer; we show an additional application of these new extractable trapdoor functions to standard digital signatures.

Velocity and acceleration analysis of complex mechanisms by graphical iteration

A simple graphical method is presented for velocity and acceleration analysis of complex mechanisms possessing low or high degree of complexity. The method is iterative in character and generally yields the solution within a few iterations. Several examples have been worked out to illustrate the method.

The authentication of electronic evidence

This thesis examines whether the rules for of evidence, which were developed around paper over centuries, are adequate for the authentication of electronic evidence. The history of documentary evidence is examined, and the nature of electronic evidence is explored, particularly recent types of electronic evidence such as social media and 'the Cloud'. The old rules are then critically applied to the varied types of electronic evidence to determine whether or not these old rules are indeed adequate.

Computing the Stochastic Complexity of Simple Probabilistic Graphical Models

Minimum Description Length (MDL) is an information-theoretic principle that can be used for model selection and other statistical inference tasks. There are various ways to use the principle in practice. One theoretically valid way is to use the normalized maximum likelihood (NML) criterion. Due to computational difficulties, this approach has not been used very often. This thesis presents efficient floating-point algorithms that make it possible to compute the NML for multinomial, Naive Bayes and Bayesian forest models. None of the presented algorithms rely on asymptotic analysis and with the first two model classes we also discuss how to compute exact rational number solutions.

Graphical simulation of Petri Nets

An interactive graphics package for modeling with Petri Nets has been implemented. It uses the VT-11 graphics terminal supported on the PDP-11/35 computer to draw, execute, analyze, edit and redraw a Petri Net. Each of the above mentioned tasks can be performed by selecting appropriate items from a menu displayed on the screen. Petri Nets with a reasonably large number of nodes can be created and analyzed using this package. The number of nodes supported may be increased by making simple changes in the program. Being interactive, the program seeks information from the user after displaying appropriate messages on the terminal. After completing the Petri Net, it may be executed step by step and the changes in the number of tokens may be observed on the screen, at each place. Some properties of Petri Nets like safety, boundedness, conservation and redundancy can be checked using this package. This package can be used very effectively for modeling asynchronous (concurrent) systems with Petri Nets and simulating the model by “graphical execution.”

Formal security analysis of the DNP3-secure authentication protocol

This thesis evaluates the security of Supervisory Control and Data Acquisition (SCADA) systems, which are one of the key foundations of many critical infrastructures. Specifically, it examines one of the standardised SCADA protocols called the Distributed Network Protocol Version 3, which attempts to provide a security mechanism to ensure that messages transmitted between devices, are adequately secured from rogue applications. To achieve this, the thesis applies formal methods from theoretical computer science to formally analyse the correctness of the protocol.

Autoregressive spectral array for graphical display of EEG data

A graphical display of the frequency content of background,electroencephalogram (EEG) activity is obtained by calculating the spectral estimates using autocorrelation autoregressive method and the classical Fourier transform method, Display of spectral content of consecutive data segments is made using hidden-line suppression technique so as to get a spectral array, The autoregressive spectral array (ASA) is found to be sensitive to baseline drift, Following baseline correction the autoregressive technique is found to be superior to the Fourier method of compressed spectral array (CSA) in detecting the transitions in the frequencies of the signal. The smoothed ASA gives a better picture of transitions and changes in the background activity, The ASA can be made to adapt to specific changes of dominant frequencies while eliminating unnecessary peaks in the spectrum. The utility,of the ASA for background EEG analysis is discussed,

Graphical method to determine the parameters of the two-parameter fracture model for concrete

To evaluate the parameters in the two-parameter fracture model, i.e. the critical stress intensity factor and critical crack tip opening displacement for the fracture of plain concrete in Mode 1 for the given test configuration and geometry, considerable computational effort is necessary. A simple graphical method has been proposed using normalized fracture parameters for the three-point bend (3PB) notched specimen and the double-edged notched (DEN) specimen. A similar graphical method is proposed to compute the maximum load carrying capacity of a specimen, using the critical fracture parameters both for 3PB and DEN configurations.

Modelling, simulation, and graphical user interface for industrial gas carburising process

A mathematical model has been developed for the gas carburising (diffusion) process using finite volume method. The computer simulation has been carried out for an industrial gas carburising process. The model's predictions are in good agreement with industrial experimental data and with data collected from the literature. A study of various mass transfer and diffusion coefficients has been carried out in order to suggest which correlations should be used for the gas carburising process. The model has been interfaced in a Windows environment using a graphical user interface. In this way, the model is extremely user friendly. The sensitivity analysis of various parameters such as initial carbon concentration in the specimen, carbon potential of the atmosphere, temperature of the process, etc. has been carried out using the model.

Low-Complexity Detection in Large-Dimension MIMO-ISI Channels Using Graphical Models

In this paper, we deal with low-complexity near-optimal detection/equalization in large-dimension multiple-input multiple-output inter-symbol interference (MIMO-ISI) channels using message passing on graphical models. A key contribution in the paper is the demonstration that near-optimal performance in MIMO-ISI channels with large dimensions can be achieved at low complexities through simple yet effective simplifications/approximations, although the graphical models that represent MIMO-ISI channels are fully/densely connected (loopy graphs). These include 1) use of Markov random field (MRF)-based graphical model with pairwise interaction, in conjunction with message damping, and 2) use of factor graph (FG)-based graphical model with Gaussian approximation of interference (GAI). The per-symbol complexities are O(K(2)n(t)(2)) and O(Kn(t)) for the MRF and the FG with GAI approaches, respectively, where K and n(t) denote the number of channel uses per frame, and number of transmit antennas, respectively. These low-complexities are quite attractive for large dimensions, i.e., for large Kn(t). From a performance perspective, these algorithms are even more interesting in large-dimensions since they achieve increasingly closer to optimum detection performance for increasing Kn(t). Also, we show that these message passing algorithms can be used in an iterative manner with local neighborhood search algorithms to improve the reliability/performance of M-QAM symbol detection.