Article
Time, computational complexity, and probability in the analysis of distance-bounding protocols
Many security protocols rely on the assumptions on the physical properties in which its protocol sessions will be carried out. For instance, Distance Bounding Protocols take into account the round trip time of messages and the transmission velocity to infer an upper bound of the distance between two agents. We classify such security protocols as Cyber-Physical. Time plays a key role in design and analysis of many of these protocols. This paper investigates the foundational differences and the impacts on the analysis when using models with discrete time and models with dense time. We show that there are attacks that can be found by models using dense time, but not when using discrete time. We illustrate this with an attack that can be carried out on most Distance Bounding Protocols. In this attack, one exploits the execution delay of instructions during one clock cycle to convince a verifier that he is in a location different from his actual position. We additionally present a probabilistic analysis of this novel attack. As a formal model for representing and analyzing Cyber-Physical properties, we propose a Multiset Rewriting model with dense time suitable for specifying cyber-physical security protocols. We introduce Circle-Configurations and show that they can be used to symbolically solve the reachability problem for our model, and show that for the important class of balanced theories the reachability problem is PSPACE-complete. We also show how our model can be implemented using the computational rewriting tool Maude, the machinery that automatically searches for such attacks.
We investigate regular realizability (RR) problems, which are the prob- lems of verifying whether intersection of a regular language – the input of the problem – and fixed language called filter is non-empty. In this pa- per we focus on the case of context-free filters. Algorithmic complexity of the RR problem is a very coarse measure of context-free languages com- plexity. This characteristic is compatible with rational dominance. We present examples of P-complete RR problems as well as examples of RR problems in the class NL. Also we discuss RR problems with context- free filters that might have intermediate complexity. Possible candidates are the languages with polynomially bounded rational indices.
The article deals with the problems of ensuring functional, informational and cyber security for vehicles and transport infrastructure facilities. The analysis of the factors causing the growth of threats to the transport sector has been carried out, the list of typical cyber attacks on the components of the transport infrastructure is given. The results of the analysis of the features of automated process control systems of technological processes of vehicles and transport infrastructure facilities are presented. Recommendations on the development of transport security systems are given taking into account the specifics of various types of transport
This volume contains the papers selected for presentation at the 18th European Symposium on Research in Computer Security (ESORICS 2013), held during September 9–13, 2013, in Egham, UK. In response to the symposium’s call for papers, 242 papers were submitted to the conference from 38 countries. These papers were evaluated on the basis of their significance, novelty, technical quality, as well as on their practical impact and/or their level of advancement of the field’s foundations. The Program Committee’s work was carri ed out electronically, yielding in- tensive discussions over a period of a few weeks. Of the papers submitted, 43 were selected for presentation at the conf erence (resulting in an acceptance rate of 18%). We note that many top-quality submissions were not selected for pre- sentation because of the high technical level of the overall submissions, and we are certain that many of these submissions will, nevertheless, be published at other competitive forums in the future.
The article analyzes the issues of legal regulation concerning liability for offences in the field of information technology (cybercrime). Author outlines the main issues of regulation in the field of information technology, examines current approaches of Russian lawyers and expressed her own proposals to resolve issues in the designated area.
It is well-known that the Dolev–Yao adversary is a powerful adversary. Besides acting as the network, intercepting, decomposing, composing and sending messages, he can remember as much information as he needs. That is, his memory is unbounded. We recently proposed a weaker Dolev–Yao like adversary, which also acts as the network, but whose memory is bounded. We showed that this Bounded Memory Dolev–Yao adversary, when given enough memory, can carry out many existing protocol anomalies. In particular, the known anomalies arise for bounded memory protocols, where although the total number of sessions is unbounded, there are only a bounded number of concurrent sessions and the honest participants of the protocol cannot remember an unbounded number of facts or an unbounded number of nonces at a time. This led us to the question of whether it is possible to infer an upper-bound on the memory required by the Dolev–Yao adversary to carry out an anomaly from the memory restrictions of the bounded protocol. This paper answers this question negatively (Theorem 8).
In a collaborative system, the agents collaborate to achieve a common goal, but they are not willing to share some sensitive private information.
The question is how much damage can be done by a malicious participant sitting inside the system.
We assume that all the participants (including internal adversaries) have bounded memory – at any moment, they can store only a fixed number of messages of a fixed size. The Dolev–Yao adversaries can compose, decompose, eavesdrop, and intercept messages, and create fresh values (nonces), but within their bounded memory.
We prove that the secrecy problem is PSPACE-complete in the bounded memory model where all actions are balanced and a potentially infinite number of the nonce updates is allowed.
We also show that the well-known security protocol anomalies (starting from the Lowe attack to the Needham–Schroeder protocol) can be rephrased within the bounded memory paradigm with the explicit memory bounds.
The book contains selected papers that were presented on PhD Summer schools on Scientific Computing jointly organized by Waterford Institute of Technology, Lomonosov Moscow State University, Kyiv National Taras Shevchenko University, Saint-Petersburg State University and Nanjing University of Technology. The schoold were mainly organized in teleconference mode and linked researchers and PhD students from several countries.
It is well-known that the Dolev-Yao adversary is a powerful adversary. Besides acting as the network, intercepting, sending, and composing messages, he can remember as much information as he needs. That is, his memory is unbounded.
We recently proposed a weaker Dolev-Yao like adversary, which also acts as the network, but whose memory is bounded. We showed that this Bounded Memory Dolev-Yao adversary, when given enough memory, can carry out many existing protocol anomalies. In particular, the known anomalies arise for bounded memory protocols, where there is only a bounded number of concurrent sessions and the honest participants of the protocol cannot remember an unbounded number of facts nor an unbounded number of nonces at a time. This led us to the question of whether it is possible to infer an upper-bound on the memory required by the Dolev-Yao adversary to carry out an anomaly from the memory restrictions of the bounded protocol. This paper answers this question negatively (Theorem 2).
The second contribution of this paper is the formalization of Progressing Collaborative Systems that may create fresh values, such as nonces. In this setting there is no unbounded adversary, although bounded memory adversaries may be present. We prove the NP-completeness of the reachability problem for Progressing Collaborative Systems that may create fresh values.
A model for organizing cargo transportation between two node stations connected by a railway line which contains a certain number of intermediate stations is considered. The movement of cargo is in one direction. Such a situation may occur, for example, if one of the node stations is located in a region which produce raw material for manufacturing industry located in another region, and there is another node station. The organization of freight traffic is performed by means of a number of technologies. These technologies determine the rules for taking on cargo at the initial node station, the rules of interaction between neighboring stations, as well as the rule of distribution of cargo to the final node stations. The process of cargo transportation is followed by the set rule of control. For such a model, one must determine possible modes of cargo transportation and describe their properties. This model is described by a finite-dimensional system of differential equations with nonlocal linear restrictions. The class of the solution satisfying nonlocal linear restrictions is extremely narrow. It results in the need for the “correct” extension of solutions of a system of differential equations to a class of quasi-solutions having the distinctive feature of gaps in a countable number of points. It was possible numerically using the Runge–Kutta method of the fourth order to build these quasi-solutions and determine their rate of growth. Let us note that in the technical plan the main complexity consisted in obtaining quasi-solutions satisfying the nonlocal linear restrictions. Furthermore, we investigated the dependence of quasi-solutions and, in particular, sizes of gaps (jumps) of solutions on a number of parameters of the model characterizing a rule of control, technologies for transportation of cargo and intensity of giving of cargo on a node station.
Event logs collected by modern information and technical systems usually contain enough data for automated process models discovery. A variety of algorithms was developed for process models discovery, conformance checking, log to model alignment, comparison of process models, etc., nevertheless a quick analysis of ad-hoc selected parts of a journal still have not get a full-fledged implementation. This paper describes an ROLAP-based method of multidimensional event logs storage for process mining. The result of the analysis of the journal is visualized as directed graph representing the union of all possible event sequences, ranked by their occurrence probability. Our implementation allows the analyst to discover process models for sublogs defined by ad-hoc selection of criteria and value of occurrence probability
Existing approaches suggest that IT strategy should be a reflection of business strategy. However, actually organisations do not often follow business strategy even if it is formally declared. In these conditions, IT strategy can be viewed not as a plan, but as an organisational shared view on the role of information systems. This approach generally reflects only a top-down perspective of IT strategy. So, it can be supplemented by a strategic behaviour pattern (i.e., more or less standard response to a changes that is formed as result of previous experience) to implement bottom-up approach. Two components that can help to establish effective reaction regarding new initiatives in IT are proposed here: model of IT-related decision making, and efficiency measurement metric to estimate maturity of business processes and appropriate IT. Usage of proposed tools is demonstrated in practical cases.