Journal of Automated Reasoning, vol. 34, Springer, pp. 295-321, 2005. DOI (I.F.: 0.875)
First-order temporal logic, the extension of first-order logic with operators dealing with time, is a powerful and expressive formalism with many potential applications. This expressive logic can be viewed as a framework in which to investigate problems specified in other logics. The monodic fragment of first-order temporal logic is a useful fragment that possesses good computational properties such as completeness and sometimes even decidability. Temporal logics of knowledge are useful for dealing with situations where the knowledge of agents in a system is involved. In this paper we present a translation from temporal logics of knowledge into the monodic fragment of first-order temporal logic. We can then use a theorem prover for monodic first-order temporal logic to prove properties of the translated formulas. This allows problems specified in temporal logics of knowledge to be verified automatically without needing a specialized theorem prover for temporal logics of knowledge. We present the translation, its correctness, and examples of its use.
Computer and Security, vol. 29, elsevier, pp. 501-514, 2010. DOI (I.F.: 0.889)
Network and device heterogeneity, nomadic mobility, intermittent connectivity and, more generally, extremely dynamic operating conditions, are major challenges in the design of security infrastructures for pervasive computing. Yet, in a ubiquitous computing environment, limitations of traditional solutions for authentication and authorization can be overcome with a pervasive public key infrastructure (pervasive-PKI). This choice allows the validation of credentials of users roaming between heterogeneous networks, even when global connectivity is lost and some services are temporarily unreachable. Proof-of-concept implementations and testbed validation results demonstrate that strong security can be achieved for users and applications through the combination of traditional PKI services with a number of enhancements like: (i) dynamic and collaborative trust model, (ii) use of attribute certificates for privilege management, and (iii) modular architecture enabling nomadic mobility and enhanced with reconfiguration capabilities.
International Journal of Information Security, Springer, 2022. DOI
Smart grids (SG) draw the attention of cyber attackers due to their vulnerabilities, which are caused by the usage of heterogeneous communication technologies and their distributed nature. While preventing or detecting cyber attacks is a well-studied field of research, making SG more resilient against such threats is a challenging task. This paper provides a classification of the proposed cyber resilience methods against cyber attacks for SG. This classification includes a set of studies that propose cyber-resilient approaches to protect SG and related cyber-physical systems against unforeseen anomalies or deliberate attacks. Each study is briefly analyzed and is associated with the proper cyber resilience technique which is given by the National Institute of Standards and Technology in the Special Publication 800-160. These techniques are also linked to the different states of the typical resilience curve. Consequently, this paper highlights the most critical challenges for achieving cyber resilience, reveals significant cyber resilience aspects that have not been sufficiently considered yet and, finally, proposes scientific areas that should be further researched in order to enhance the cyber resilience of SG.
ACM Transactions on Privacy and Security (TOPS), vol. 25, issue 2, no. 10, Association for Computer Machinery (ACM), pp. 1 - 29, 05/2022. DOI (I.F.: 1.909)
Proximity attacks allow an adversary to uncover the location of a victim by repeatedly issuing queries with fake location data. These attacks have been mostly studied in scenarios where victims remain static and there are no constraints that limit the actions of the attacker. In such a setting, it is not difficult for the attacker to locate a particular victim and quantifying the effort for doing so is straightforward. However, it is far more realistic to consider scenarios where potential victims present a particular mobility pattern. In this paper, we consider abstract (constrained and unconstrained) attacks on services that provide location information on other users in the proximity. We derive strategies for constrained and unconstrained attackers, and show that when unconstrained they can practically achieve success with theoretically optimal effort. We then propose a simple yet effective constraint that may be employed by a proximity service (for example, running in the cloud or using a suitable two-party protocol) as countermeasure to increase the effort for the attacker several orders of magnitude both in simulated and real-world cases.