Denial of Service (DoS) attacks constitute a major security threat to today’s Internet. This challenge is especially pertinent to the Internet of Things (IoT) as devices have less computing power, memory and security mechanisms to mitigate DoS attacks. This paper presents a model that mimics the unique characteristics of a network of IoT devices, including components of the system implementing ‘Crypto Puzzles’ - a DoS mitigation technique.

Verification of neural networks is currently a hot topic in automated theorem proving. However,there is currently no general methodology for bridging the gap between verifiers and interactive theorem provers (ITPs). In this paper we present Vehicle, our solution to this problem. Vehicle is equipped with an expressive domain specific language for stating neural network specifications which can be compiled to both verifiers and ITPs.

Denial of service attacks are especially pertinent to the internet of things as devices have less computing power, memory and security mechanisms to defend against them. The task of mitigating these attacks must therefore be redirected from the device onto a network monitor. Through bespoke datasets generated by the model, the IDS is able to predict a wide spectrum of real-world attacks, and as demonstrated by an experiment construct more predictive datasets at a fraction of the time of other more standard techniques.

In this article, we review works on IDS specifically for these kindsof devices from 2008 to 2018, collecting a total of 51 different IDS papers. We summarise the current themes of the field, summarisethe techniques employed to train and deploy the IDSs and provide a qualitative evaluations of these approaches. While these worksprovide valuable insights and solutions for sub-parts of these constraints, we discuss the limitations of these solutions as a whole, inparticular what kinds of attacks these approaches struggle to detect and the setup limitations that are unique to this kind of system

We present MetaCP, a tool to aid the cryptographer throughout the process of designing and modelling a communication protocol suitable for formal verification. The crucial innovative aspect of the tool is its data-centric approach, where protocol specification is stored in a structured way rather than in natural languages to facilitate its interpretation to multiple target languages. By improving the expressiveness of the specification data structure we extend the tool to export to an additional formal language, i.e. ProVerif, as well as a C++ implementation..

Cyber-Physical Systems (CPS) are present in many settings addressing a myriad of purposes. Examples are Internet-of-Things (IoT) or sensing software embedded in appliances or even specialised meters that measure and respond to electricity demands in smart grids.Due to their pervasive nature, they are usually chosen as recipients for larger scope cyber-security attacks. Our approach models Coordinated Load-Changing Attacks (CLCA) also referred as GridLock or BlackIoT, against a theoretical power grid, containing various types of power plants. It employs Continuous-Time Markov Chains where elements such as Power Plants and Botnets are modelled under normal or attack situations to evaluate the effect of CLCA in power reliant infrastructures.

The study introduces an automated trading system for S&P500 E-mini futures (ES) based on state-of-the-art machine learning. Concretely: we extract a set of scenarios from the tick market data to train the models and further use the predictions to statistically assess the soundness of the approach.

Financial markets are a source of non-stationary multidimensional time series which has been drawing attention for decades. Each financial instrument has its specific changing over time properties, making their analysis a complex task. In this study we propose a volume-based data pre-processing method for making financial time series more suitable for machine learning pipelines. We use a statistical approach for assessing the performance of the method, improving rigour and reproducibility.

We propose MetaCP, a Meta Cryptography Protocol verification tool, as an automated tool simplifying the design of security protocols through a graphical interface. In this paper, we showcase the effectiveness of this novel approach by demonstrating how easy MetaCP makes it to design and verify a protocol going from the graphical design to formally verified protocol using a Tamarin prover plugin.

As our daily lives become ever more connected, the need for security becomes more important. This need is, however, in conflict withthe way most Internet of Things (IoT) devices are designed. These devices often have limited computing power, memory, and security mechanisms to defend against a range of attacks. The protocol designer must therefore take all these constraints into considerationwhen making IoT security design decisions. In this paper, we use the formal analysis tool Tamarin to analyze the ACE-OAuth protocol, and illustrate how protocol designers can analyze their own extensions

In a nutshell, a LISA model consists of acollection of Markov Decision Processes (MDP), representing the IoT network, the attackers, and some processes monitor-ing the security metrics under consideration. A trace of theLISA model (corresponding to a sequence of actions of thedifferent MDPs) should match a trace of the actual system, and conversely, such that it becomes possible to train a NIDS for the actual system on the traces of the LISA model.