4th Conference on Principles of Security and Trust (POST 2015)
4th International Conference, POST 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings
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 a novel 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 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. Finally, we show that for the important class of balanced theories the reachability problem is PSPACE-complete.
Development of information and communication technologies (ICT) is a key aspect of modernising the Russian economy. Russia is gradually approaching developed countries in terms of ICT infrastructure and Internet access. Along with opportunities opened by the rapid development and proliferation of ICT, systemic threats to security of critical components of public and private infrastructures are becoming increasingly more serious. Accordingly, achieving an acceptable level of supply chains’ cyber security, and managing relevant risks, are turning into top priorities of the national policy.
It is our great pleasure to welcome you to the Fourth ACM Workshop on Cyber-Physical Systems Security and PrivaCy (CPS-SPC) in conjunction with the 25th ACM Conference on Computer and Communications Security (CCS) in Toronto, Canada.
Our increased dependency on cyber-physical systems (CPS) has amplified concerns of cyber attacks on these systems. These transformative attack methods require additional research into secure control systems and related architectures of CPS. The majority of the published literature addressing the security and privacy of CPS reflect a field that is still developing. As such, the overall principles, models, and theories for securing CPS have not yet emerged. The CPS-SPC workshop series provides a focal point for the research community to begin addressing the security and privacy of CPS in a comprehensive and interdisciplinary manner and, in tandem with other efforts, build a comprehensive research roadmap. As a workshop, we expect to attract papers that reflect new research directions in CPS security and privacy as well as early results based on "works in progress".
This year's workshop builds on the foundation laid last year to become one of the premier forums for presentation of interdisciplinary research results and experience reports at the interface of control theory, information security, embedded and real-time systems and human factors applied to CPS. The mission of the workshop is to create a community of researchers focusing on diverse aspects of CPS Security and Privacy, and to provide researchers and practitioners a premier forum to share their perspectives with others interested in interdisciplinary approaches to solve the challenging security and privacy problems in CPS.
The workshop attracted 22 submissions from across 15 countries, and all papers were reviewed by at least three program committee members. 8 full papers and 2 short papers were accepted leading to a 45% acceptance rate.
Distance-bounding (DB) protocols protect against relay attacks on proximity-based access control systems. In a DB protocol, the verifier computes an upper bound on the distance to the prover by measuring the time-of-flight of exchanged messages. DB protocols are, however, vulnerable to distance fraud, in which a dishonest prover is able to manipulate the distance bound computed by an honest verifier. Despite their conceptual simplicity, devising a formal characterization of DB protocols and distance fraud attacks that is amenable to automated formal analysis is non-trivial, primarily because of their real-time and probabilistic nature. In this work, we introduce a generic, computational model, based on Rewriting Logic, for formally analyzing various forms of distance fraud, including recently identified timing attacks, on the Hancke-Kuhn family of DB protocols through statistical model checking. While providing an insightful formal characterization on its own, the model enables a practical formal analysis method that can help system designers bridge the gap between conceptual descriptions and low-level designs. In addition to accurately confirming known results, we use the model to define new attack strategies and quantitatively evaluate their effectiveness under realistic assumptions that would otherwise be difficult to reason about manually.
2018 IEEE 12th International Conference on Application of Information and Communication Technologies (AICT)
Copyright © 2018 by the Institute of Electrical and Electronics Engineers, Inc. All rights reserved.
Copyright and Reprint Permission
Abstracting is permitted with credit to the source. Libraries are permitted to photocopy beyond the limit of U.S. copyright law, for private use of patrons, those articles in this volume that carry a code at the bottom of the first page, provided that the per-copy fee indicated in the code is paid through the Copyright Clearance Center, 222 Rosewood Drive, Danvers, MA 01923.
Other copying, reprint, or reproduction requests should be addressed to IEEE Copyrights Manager, IEEE
Service Center, 445 Hoes Lane, P.O. Box 1331, Piscataway, NJ 08855-1331.
IEEE Catalog Number: CFP1856H-PRT
Additional copies of this publication are available from
Curran Associates, Inc.
57 Morehouse Lane
Red Hook, NY 12571 USA
+1 845 758 0400
+1 845 758 2633 (FAX)
© Designed by the AICT2018 Publication Team, 2018.
The article reviews the main events of the Third International Summer School on Cyber Law, organized by the Laboratory of information law (National Research University Higher School of Economics, Russia).
This year applications for participation in the summer school were submitted from the UK, Italy, Germany, Slovakia, Armenia, India, Belarus, Kyrgyzstan and from different cities of the Russian Federation. In the framework of the summer school the most current research trends in the field of information law and intellectual property law were touched, new problems and new issues were raised, and solutions were suggested. Among the guests of the summer school were representatives of IBM, Yandex, Google, MegaFon, Wargaming.net, Kaspersky lab, as well as professors of foreign universities.
Intense program of the summer school included a discussions on legal aspects of development and introduction of cognitive systems, legal regulation in the field of computer games, novelties of the Russian information legislation, relevant issues of telecommunication law and copyright, legal aspects of cyber security, as well as other important legal issues in IT/IP sphere.
Large attention of participants was paid to the problems of enforcing the new Russian legislation on the requirements to the information dissemination organizers on the Internet and popular bloggers. In light of enacting this legislation the questions of websites blocking were raised again. In the field of telecommunications law the issues of legal regulation of OTT-services were the most disputable. The legal aspects of the computer games industry which were discussed in the summer school include the issues of legal protection of computer games as objects of intellectual property, as well as the issues of e-commerce in the area of online computer games.
A special event in the framework of the summer school program was the master-class of foreign professors on how to write articles in English to international peer-reviewed journals.
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.
Recent work on structure-preserving signatures studies optimality of these schemes in terms of the number of group elements needed in the verification key and the signature, and the number of pairing-product equations in the verification algorithm. While the size of keys and signatures is crucial for many applications, another important aspect to consider for performance is the time it takes to verify a given signature. By far, the most expensive operation during verification is the computation of pairings. However, the concrete number of pairings that one needs to compute is not captured by the number of pairing-product equations considered in earlier work. To fill this gap, we consider the question of what is the minimal number of pairings that one needs to compute in the verification of structure-preserving signatures. First, we prove lower bounds for schemes in the Type II setting that are secure under chosen message attacks in the generic group model, and we show that three pairings are necessary and that at most one of these pairings can be precomputed. We also extend our lower bound proof to schemes secure under random message attacks and show that in this case two pairings are still necessary. Second, we build an automated tool to search for schemes matching our lower bounds. The tool can generate automatically and exhaustively all valid structure-preserving signatures within a user-specified search space, and analyze their (bounded) security in the generic group model. Interestingly, using this tool, we find a new randomizable structure-preserving signature scheme in the Type II setting that is optimal with respect to the lower bound on the number of pairings, and also minimal with respect to the number of group operations that have to be computed during verification.
Activities such as clinical investigations (CIs) or financial processes are subject to regulations to ensure quality of results and avoid negative consequences. Regulations may be imposed by multiple governmental agencies as well as by institutional policies and protocols. Due to the complexity of both regulations and activities, there is great potential for violation due to human error, misunderstanding, or even intent. Executable formal models of regulations, protocols and activities can form the foundation for automated assistants to aid planning, monitoring and compliance checking. We propose a model based on multiset rewriting where time is discrete and is specified by timestamps attached to facts. Actions, as well as initial, goal and critical states may be constrained by means of relative time constraints. Moreover, actions may have non-deterministic effects, i.e. they may have different outcomes whenever applied. We present a formal semantics of our model based on focused proofs of linear logic with definitions. We also determine the computational complexity of various planning problems. Plan compliance problem, for example, is the problem of finding a plan that leads from an initial state to a desired goal state without reaching any undesired critical state. We consider all actions to be balanced, i.e. their pre- and post-conditions have the same number of facts. Under this assumption on actions, we show that the plan compliance problem is PSPACE-complete when all actions have only deterministic effects and is EXPTIME-complete when actions may have non-deterministic effects. Finally, we show that the restrictions on the form of actions and time constraints taken in the specification of our model are necessary for decidability of the planning problems.
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 traﬃc 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 ﬁnal 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 ﬁnite-dimensional system of diﬀerential 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 diﬀerential 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
The geographic information system (GIS) is based on the first and only Russian Imperial Census of 1897 and the First All-Union Census of the Soviet Union of 1926. The GIS features vector data (shapefiles) of allprovinces of the two states. For the 1897 census, there is information about linguistic, religious, and social estate groups. The part based on the 1926 census features nationality. Both shapefiles include information on gender, rural and urban population. The GIS allows for producing any necessary maps for individual studies of the period which require the administrative boundaries and demographic information.
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.