Searcharxiv⌕ Search

arXiv subjects

Luca Viganò

Publications and source records attributed to Luca Viganò.

At least 19 recordsLinked to original sources
arXiv2026

Policies for Fair Exchanges of Resources

People increasingly use digital platforms to exchange resources in accordance with some policies stating what resources users offer and what they require in return. In this paper, we propose a formal model of these environments, focussing on how users' policies are defined and enforced, so ensuring that malicious users cannot take advantage of honest ones. To that end, we introduce the declarative policy language MuAC and equip it with a formal semantics. To determine if a resource exchange is fair, i.e., if it respects the MuAC policies in force, we introduce the non-standard logic MuACL that combines non-linear, linear and contractual aspects, and prove it decidable. Notably, the operator for contractual implication of MuACL is not expressible in linear logic. We define a semantics preserving compilation of MuAC policies into MuACL, thus establishing that exchange fairness is reduced to finding a proof in MuACL. Finally, we show how this approach can be put to work on a blockchain to exchange non-fungible tokens.

cs.LO↗
arXiv2026

Trajectory-informed graph-based clustering for longitudinal cancer subtyping

Cancer subtyping plays a crucial role in informing prognosis and guiding personalized treatment strategies. However, conventional subtyping approaches often rely on static, biopsy-derived scores that hardly capture the biological heterogeneity and temporal evolution of the disease. In this study, we propose a novel trajectory-informed clustering method for cancer subtyping that integrates multi-modal clinical data and longitudinal patient trajectories. Our method constructs a patient similarity graph using time-varying imaging-derived features, clinical covariates, and transitions among key clinical states such as therapy, surveillance, relapse, and death. This graph structure enables the identification of patient subgroups that are not only phenotypically and genotypically distinct but also aligned with patterns of disease progression. We position our approach within the landscape of existing subtyping methods and highlight its advantages in terms of temporal modeling and graph-based interpretability. Through simulation studies and application to a real world dataset of liver metastases, we demonstrate the ability of our framework to uncover clinically relevant subtypes with distinct prognostic trajectories. Our results underscore the potential of trajectory-informed clustering to enhance personalized oncology by bridging cross-sectional biomarkers with dynamic disease evolution.

stat.ME↗
arXiv2025

Can Large Language Models Automate Phishing Warning Explanations? A Controlled Experiment on Effectiveness and User Perception

Phishing has become a prominent risk in modern cybersecurity, often used to bypass technological defences by exploiting predictable human behaviour. Warning dialogues are a standard mitigation measure, but the lack of explanatory clarity and static content limits their effectiveness. In this paper, we report on our research to assess the capacity of Large Language Models (LLMs) to generate clear, concise, and scalable explanations for phishing warnings. We carried out a large-scale between-subjects user study (N = 750) to compare the influence of warning dialogues supplemented with manually generated explanations against those generated by two LLMs, Claude 3.5 Sonnet and Llama 3.3 70B. We investigated two explanatory styles (feature-based and counterfactual) for their effects on behavioural metrics (click-through rate) and perceptual outcomes (e.g., trust, risk, clarity). The results provide empirical evidence that LLM-generated explanations achieve a level of protection statistically comparable to expert-crafted messages, effectively automating a high-cost task. While Claude 3.5 Sonnet showed a trend towards reducing click-through rates compared to manual baselines, Llama 3.3, despite being perceived as clearer, did not yield the same behavioral benefits. Feature-based explanations were more effective for genuine phishing attempts, whereas counterfactual explanations diminished false-positive rates. Other variables, such as workload, gender, and prior familiarity with warning dialogues, significantly moderated the effectiveness of warnings. These results indicate that LLMs can be used to automatically build explanations for warning users against phishing, and that such solutions are scalable, adaptive, and consistent with human-centred values.

cs.CR↗
arXiv2024

APOLLO: A GPT-based tool to detect phishing emails and generate explanations that warn users

Phishing is one of the most prolific cybercriminal activities, with attacks becoming increasingly sophisticated. It is, therefore, imperative to explore novel technologies to improve user protection across both technical and human dimensions. Large Language Models (LLMs) offer significant promise for text processing in various domains, but their use for defense against phishing attacks still remains scarcely explored. In this paper, we present APOLLO, a tool based on OpenAI's GPT-4o to detect phishing emails and generate explanation messages to users about why a specific email is dangerous, thus improving their decision-making capabilities. We have evaluated the performance of APOLLO in classifying phishing emails; the results show that the LLM models have exemplary capabilities in classifying phishing emails (97 percent accuracy in the case of GPT-4o) and that this performance can be further improved by integrating data from third-party services, resulting in a near-perfect classification rate (99 percent accuracy). To assess the perception of the explanations generated by this tool, we also conducted a study with 20 participants, comparing four different explanations presented as phishing warnings. We compared the LLM-generated explanations to four baselines: a manually crafted warning, and warnings from Chrome, Firefox, and Edge browsers. The results show that not only the LLM-generated explanations were perceived as high quality, but also that they can be more understandable, interesting, and trustworthy than the baselines. These findings suggest that using LLMs as a defense against phishing is a very promising approach, with APOLLO representing a proof of concept in this research direction.

cs.HC↗
arXiv2024

A Logic for Policy Based Resource Exchanges in Multiagent Systems

In multiagent systems autonomous agents interact with each other to achieve individual and collective goals. Typical interactions concern negotiation and agreement on resource exchanges. Modeling and formalizing these agreements pose significant challenges, particularly in capturing the dynamic behaviour of agents, while ensuring that resources are correctly handled. Here, we propose exchange environments as a formal setting where agents specify and obey exchange policies, which are declarative statements about what resources they offer and what they require in return. Furthermore, we introduce a decidable extension of the computational fragment of linear logic as a fundamental tool for representing exchange environments and studying their dynamics in terms of provability.

cs.LO↗
arXiv2024

A Formal Approach For Modelling And Analysing Surgical Procedures (Extended Version)

Surgical procedures are often not "standardised" (i.e., defined in a unique and unambiguous way), but rather exist as implicit knowledge in the minds of the surgeon and the surgical team. This reliance extends to pre-surgery planning and effective communication during the procedure. We introduce a novel approach for the formal and automated analysis of surgical procedures, which we model as security ceremonies, leveraging well-established techniques developed for the analysis of such ceremonies. Mutations of a procedure are used to model variants and mistakes that members of the surgical team might make. Our approach allows us to automatically identify violations of the intended properties of a surgical procedure.

cs.CR↗
arXiv2022

Automatic Fair Exchanges

In a decentralized environment, exchanging resources requires users to bargain until an agreement is found. Moreover, human agreements involve a combination of collaborative and selfish behavior and often induce circularity, complicating the evaluation of exchange requests. We introduce MuAC, a policy language that allows users to state in isolation under which conditions they are open to grant their resources and what they require in return. In MuAC, exchange requests are evaluated automatically with the guarantee that the only exchanges that will take place are those that mutually satisfy users' conditions. Moreover, MuAC can be used as an enforcement mechanism to prevent users from cheating. As a proof of concept, we implement a blockchain smart contract that allows users to exchange their non-fungible tokens.

cs.CR↗
arXiv2021

Don't Tell Me The Cybersecurity Moon Is Shining... (Cybersecurity Show And Tell)

"Show, don't tell" has become the literary commandment for any writer. It applies to all forms of fiction, and to non-fiction, including scientific writing, where it lies at the heart of many scientific communication and storytelling approaches. In this paper, I discuss how "show \emph{and} tell" is actually often the best approach when one wants to present, teach or explain complicated ideas such as those underlying notions and results in mathematics and science, and in particular in cybersecurity. I discuss how different kinds of artworks can be used to explain cybersecurity and I illustrate how telling (i.e., explaining notions in a formal, technical way) can be paired with showing through visual storytelling or other forms of storytelling. I also discuss four categories of artworks and the explanations they help provide.

cs.CR↗
arXiv2021

A Formal Approach to Physics-Based Attacks in Cyber-Physical Systems (Extended Version)

We apply formal methods to lay and streamline theoretical foundations to reason about Cyber-Physical Systems (CPSs) and physics-based attacks, i.e., attacks targeting physical devices. We focus on a formal treatment of both integrity and denial of service attacks to sensors and actuators of CPSs, and on the timing aspects of these attacks. Our contributions are fourfold. (1)~We define a hybrid process calculus to model both CPSs and physics-based attacks. (2)~We formalise a threat model that specifies MITM attacks that can manipulate sensor readings or control commands in order to drive a CPS into an undesired state, and we provide the means to assess attack tolerance/vulnerability with respect to a given attack. (3)~We formalise how to estimate the impact of a successful attack on a CPS and investigate possible quantifications of the success chances of an attack. (4)~We illustrate our definitions and results by formalising a non-trivial running example in Uppaal SMC, the statistical extension of the Uppaal model checker; we use Uppaal SMC as an automatic tool for carrying out a static security analysis of our running example in isolation and when exposed to three different physics-based attacks with different impacts.

cs.LO↗
arXiv2019

Time-Stamped Claim Logic

The main objective of this paper is to define a logic for reasoning about distributed time-stamped claims. Such a logic is interesting for theoretical reasons, i.e., as a logic per se, but also because it has a number of practical applications, in particular when one needs to reason about a huge amount of pieces of evidence collected from different sources, where some of the pieces of evidence may be contradictory and some sources are considered to be more trustworthy than others. We introduce the Time-Stamped Claim Logic including a sound and complete sequent calculus that allows one to reduce the size of the collected set of evidence and removes inconsistencies, i.e., the logic ensures that the result is consistent with respect to the trust relations considered. In order to show how Time-Stamped Claim Logic can be used in practice, we consider a concrete cyber-attribution case study.

cs.LO↗
arXiv2019

It could be worse, it could be raining: reliable automatic meteorological forecasting

Meteorological forecasting provides reliable prediction about the future weather within a given interval of time. Meteorological forecasting can be viewed as a form of hybrid diagnostic reasoning and can be mapped onto an integrated conceptual framework. The automation of the forecasting process would be helpful in a number of contexts, in particular: when the amount of data is too wide to be dealt with manually; to support forecasters education; when forecasting about underpopulated geographic areas is not interesting for everyday life (and then is out from human forecasters' tasks) but is central for tourism sponsorship. We present logic MeteoLOG, a framework that models the main steps of the reasoner the forecaster adopts to provide a bulletin. MeteoLOG rests on several traditions, mainly on fuzzy, temporal and probabilistic logics. On this basis, we also introduce the algorithm Tournament, that transforms a set of MeteoLOG rules into a defeasible theory, that can be implemented into an automatic reasoner. We finally propose an example that models a real world forecasting scenario.

cs.AI↗
arXiv2018

Smart Humans... WannaDie?

It won't be long until our prostheses, ECG personal monitors, subcutaneous insulin infusors, glasses, etc. become devices of the Internet of Things (IoT), always connected for monitoring, maintenance, charging and tracking. This will be the dawn of the Smart Human, not just a user of the IoT but a Thing in the Internet. How long would it then take for hackers to attack us like they have been attacking IoT devices? What would happen if hackers were able to blackmail us threatening our IoT body parts? Smart Humans may become victims of the devastating attack of WannaDie, a new ransomware that could provide the plot-line for a possible future episode of the Black Mirror TV series.

cs.CY↗
arXiv2018

Schrödinger's Man

What if someone built a "box" that applies quantum superposition not just to quantum bits in the microscopic but also to macroscopic everyday "objects", such as Schrödinger's cat or a human being? If that were possible, and if the different "copies" of a man could exploit quantum interference to synchronize and collapse into their preferred state, then one (or they?) could in a sense choose their future, win the lottery, break codes and other security devices, and become king of the world, or actually of the many-worlds. We set up the plot-line of a new episode of Black Mirror to reflect on what might await us if one were able to build such a technology.

cs.OH↗
arXiv2018

MMM: May I Mine Your Mind?

Consider the following set-up for the plot of a possible future episode of the TV series Black Mirror: human brains can be connected directly to the net and MiningMind Inc. has developed a technology that merges a reward system with a cryptojacking engine that uses the human brain to mine cryptocurrency (or to carry out some other mining activity). Part of our brain will be committed to cryptographic calculations (mining), leaving the remaining part untouched for everyday operations, i.e., for our brain's normal daily activity. In this short paper, we briefly argue why this set-up might not be so far fetched after all, and explore the impact that such a technology could have on our lives and our society.

cs.CY↗
arXiv2018

Explainable Security

The Defense Advanced Research Projects Agency (DARPA) recently launched the Explainable Artificial Intelligence (XAI) program that aims to create a suite of new AI techniques that enable end users to understand, appropriately trust, and effectively manage the emerging generation of AI systems. In this paper, inspired by DARPA's XAI program, we propose a new paradigm in security research: Explainable Security (XSec). We discuss the ``Six Ws'' of XSec (Who? What? Where? When? Why? and How?) and argue that XSec has unique and complex characteristics: XSec involves several different stakeholders (i.e., the system's developers, analysts, users and attackers) and is multi-faceted by nature (as it requires reasoning about system model, threat model and properties of security, privacy and trust as well as about concrete attacks, vulnerabilities and countermeasures). We define a roadmap for XSec that identifies several possible research directions.

cs.CR↗
arXiv2018

Privacy, Security and Trust in the Internet of Neurons

Arpanet, Internet, Internet of Services, Internet of Things, Internet of Skills. What next? We conjecture that in 15-20 years from now we will have the Internet of Neurons, a new Internet paradigm in which humans will be able to connect bi-directionally to the net using only their brain. The Internet of Neurons will provide new, tremendous opportunities thanks to constant access to unlimited information. It will empower all those outside of the technical industry, actually it will empower all human beings, to access and use technological products and services as everybody will be able to connect, even without possessing a laptop, a tablet or a smartphone. The Internet of Neurons will thus ultimately complete the currently still immature democratization of knowledge and technology. But it will also bring along several enormous challenges, especially concerning security (as well as privacy and trust). In this paper we speculate on the worldwide deployment of the Internet of Neurons by 2038 and brainstorm about its disruptive impact, discussing the main technological (and neurological) breakthroughs required to enable it, the new opportunities it provides and the security challenges it raises. We also elaborate on the novel system models, threat models and security properties that are required to reason about privacy, security and trust in the Internet of Neurons.

cs.CY↗
arXiv2018

A Formal Approach to Analyzing Cyber-Forensics Evidence

The frequency and harmfulness of cyber-attacks are increasing every day, and with them also the amount of data that the cyber-forensics analysts need to collect and analyze. In this paper, we propose a formal analysis process that allows an analyst to filter the enormous amount of evidence collected and either identify crucial information about the attack (e.g., when it occurred, its culprit, its target) or, at the very least, perform a pre-analysis to reduce the complexity of the problem in order to then draw conclusions more swiftly and efficiently. We introduce the Evidence Logic EL for representing simple and derived pieces of evidence from different sources. We propose a procedure, based on monotonic reasoning, that rewrites the pieces of evidence with the use of tableau rules, based on relations of trust between sources and the reasoning behind the derived evidence, and yields a consistent set of pieces of evidence. As proof of concept, we apply our analysis process to a concrete cyber-forensics case study.

cs.CR↗