We present a decision procedure for verifying whether a protocol respects privacy goals, given a bound on the number of transitions. We consider multi message-analysis problems , where the intruder does not know exactly the structure of the messages but rather knows several possible structures and that the real execution corresponds to one of them. This allows for modeling a large class of security protocols, with standard cryptographic operators, non-determinism, branching and statefulness. Our first contribution is the definition of a decision procedure for a fragment of alpha-beta privacy. Moreover, we have implemented a prototype tool as a proof-of-concept and a first step towards automation. Our second contribution is to show that, for a class of protocols satisfying certain syntactic conditions, it is sound to restrict the intruder model to a typed model, where the intruder only sends well-typed messages. Our typing result holds for an unbounded number of transitions.

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.

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 GPT-4o has exemplary capabilities in classifying phishing emails (97% accuracy) and that this performance can be further improved by integrating data from third-party services, resulting in a near-perfect classification rate (99% 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.

We present a decision procedure for verifying whether a protocol respects privacy goals, given a bound on the number of transitions. We consider multi message-analysis problems, where the intruder does not know exactly the structure of the messages but rather knows several possible structures and that the real execution corresponds to one of them. This allows for modeling a large class of security protocols, with standard cryptographic operators, non-determinism and branching. Our main contribution is the definition of a decision procedure for a fragment of alpha-beta privacy. Moreover, we have implemented a prototype tool as a proof-of-concept and a first step towards automation.

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.

There is an increasing number of cyber-systems (e.g., systems for payment, transportation, voting, critical infrastructures) whose security depends intrinsically on human users. In this paper, we introduce a novel approach for the formal and automated analysis of security ceremonies. A security ceremony expands a security protocol to include human nodes alongside computer nodes, with communication links that comprise user interfaces, human-to-human communication and transfers of physical objects that carry data, and thus a ceremony’s security analysis should include, in particular, the mistakes that human users might make when participating actively in the ceremony. Our approach defines mutation rules that model possible behaviors of a human user, automatically generates mutations in the behavior of the other agents of the ceremony to match the human-induced mutations, and automatically propagates these mutations through the whole ceremony. This allows for the analysis of the original ceremony specification and its possible mutations, which may include the way in which the ceremony has actually been implemented or could be implemented. To automate our approach, we have developed the tool X-Men, which is a prototype that builds on top of Tamarin, one of the most common tools for the automatic unbounded verification of security protocols. As a proof of concept, we have applied our approach to three real-life case studies, uncovering a number of concrete vulnerabilities. Some of these vulnerabilities were so far unknown, whereas others had so far been discovered only by empirical observation of the actual ceremony execution or by directly formalizing alternative models of the ceremony by hand, but X-Men instead allowed us to find them automatically.

We show that privacy can be formalized as a reachability problem. We introduce a transaction-process formalism for distributed systems that can exchange cryptographic messages (in a black-box cryptography model). Our formalism includes privacy variables chosen non-deterministically from finite domains (e.g., candidates in a voting protocol), it can work with long-term mutable states (e.g., a hash-key chain) and allows one to specify consciously released information (e.g., number of votes and the result). We discuss examples, e.g., problems of linkability, and the core of the privacy-preserving proximity tracing system DP-3T.

Successful attacks on information systems often exploit not only IT systems and networks, but also the human element in the system.It is vital to understand technical vulnerabilities and how user behavior contributes to their exploitation, but also poorly designed user interfaces, and unclear or unrealistic security policies.To improve the security of systems, technology and policies must consider the characteristics of the users, where research in social sciences and usable security has demonstrated that user behavior involved in security exploits can be understood from cognitive, emotional, and social perspectives.When there is a good "fit" of technology to users, workable security policies and targeted behavioral support can augment technical security.Finding the right balance between technical and social security measures remains, however, largely unexplored, and different security communities (theoretical security, systems security, usable security, and security management) rarely work together.There remains a need for focused, holistic research in socio-technical security, and the respective communities tend to offload on each other parts of problems that they consider to be out of scope.This is an attitude that results in deficient or unsuitable security solutions.The research domain of socio-technical security was born after many realized that practical attacks against information services often succeed because of a combination of social engineering practices and technical skills.Often, such attacks were possible because of vulnerable security mechanisms, ill-designed system interfaces, unusable security policies, or carelessly conceived human computer ceremonies -and not because humans just "don't get security right", as it was wrongly put not a long time ago.In 2011, Giampaolo Bella and Gabriele Lenzini created the international Workshop on "Socio-Technical Aspects in Security and Trust" (STAST) to gather experts in security and experts in social science with an interest in security, and thus foster an interdisciplinary discussion on how to model and analyze the socio-technical aspects of modern security systems and on how to protect such systems from socio-technical threats and attacks.Since then, the workshop has taken place annually, shortening its name to "Socio-Technical Aspects in Security", but continuing to stimulate an active exchange of ideas and experiences from different communities of researchers in order to identify weaknesses potentially emerging from poor usability designs and policies, from social engineering, and from deficiencies hidden in flawed interfaces and implementations.STAST has been bringing together experts in computer security and in cognitive, social, and behavioral sciences; it has been collecting the state of the art, identifying open and emerging problems, and proposing future research directions.

There is an increasing number of cyber-systems (e.g., payment, transportation, voting, critical-infrastructure systems) whose security depends intrinsically on human users. A security ceremony expands a security protocol with everything that is considered out-of-band to it, including, in particular, the mistakes that human users might make when participating actively in the security ceremony. In this paper, we introduce a novel approach for the formal analysis of security ceremonies. Our approach defines mutation rules that model possible behaviors of a human user, and automatically generates mutations in the behavior of the other agents of the ceremony to match the human-induced mutations. This allows for the analysis of the original ceremony specification and its possible mutations, which may include the way in which the ceremony has actually been implemented. To automate our approach, we have developed the tool X-Men, which is a prototype that extends Tamarin, one of the most common tools for the automatic unbounded verification of security protocols. As a proof of concept, we have applied our approach to two real-life case studies, uncovering a number of concrete vulnerabilities.

We propose a formal and automated approach that allows one to (i) reason about vulnerabilities of web applications and (ii) combine multiple vulnerabilities for the identification of complex, multi-stage attacks. We have developed WAFEx, an automatic tool that implements our approach and we show its efficiency by applying it to real-world case studies. WAFEx was able to generate, and exploit, previously unknown attacks.

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 to drive a CPS into an undesired state; we group these attacks into classes and provide the means to assess attack tolerance/vulnerability with respect to a given class of attacks, based on a proper notion of most powerful physics-based 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 U PPAAL SMC, the statistical extension of the U PPAAL model checker; we use U PPAAL 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.

Over the last few years, there has been an almost exponential increase in the number of mobile applications that deal with sensitive data, such as applications for e-commerce or health. When dealing with sensitive data, classical authentication solutions based on username-password pairs are not enough, and multi-factor authentication solutions that combine two or more authentication factors of different categories are required instead. Even if several solutions are currently used, their security analyses have been performed informally or semiformally at best, and without a reference model and a precise definition of the multi-factor authentication property. This makes a comparison among the different solutions both complex and potentially misleading. In this article, we first present the design of two reference models for native applications based on the requirements of two real-world use-case scenarios. Common features between them are the use of one-time password approaches and the support of a single sign-on experience. Then, we provide a formal specification of our threat model and the security goals, and discuss the automated security analysis that we performed. Our formal analysis validates the security goals of the two reference models we propose and provides an important building block for the formal analysis of different multi-factor authentication solutions.

A Simple Temporal Network (STN) consists of time points modeling temporal events and constraints modeling the minimal and maximal temporal distance between them. A Simple Temporal Network with Decisions (STND) extends an STN by adding decision time points to model temporal plans with decisions. A decision time point is a special kind of time point that once executed allows for deciding a truth value for an associated Boolean proposition. Furthermore, STNDs label time points and constraints by conjunctions of literals saying for which scenarios (i.e., complete truth value assignments to the propositions) they are relevant. Thus, an STND models a family of STNs each obtained as a projection of the initial STND onto a scenario. An STND is consistent if there exists a consistent scenario (i.e., a scenario such that the corresponding STN projection is consistent). Recently, a hybrid SAT-based consistency checking algorithm (HSCC) was proposed to check the consistency of an STND. Unfortunately, that approach lacks experimental evaluation and does not allow for the synthesis of all consistent scenarios. In this paper, we propose an incremental HSCC algorithm for STNDs that (i) is faster than the previous one and (ii) allows for the synthesis of all consistent scenarios and related early execution schedules (offline temporal planning). Then, we carry out an experimental evaluation with KAPPA, a tool that we developed for STNDs. Finally, we prove that STNDs and disjunctive temporal networks (DTNs) are equivalent.

Conditional simple temporal networks with uncertainty (CSTNUs) allow for the representation of temporal plans subject to both conditional constraints and uncertain durations. Dynamic controllability (DC) of CSTNUs ensures the existence of an execution strategy able to execute the network in real time (i.e., scheduling the time points under control) depending on how these two uncontrollable parts behave. However, CSTNUs do not deal with resources. In this paper, we define conditional simple temporal networks with uncertainty and resources (CSTNURs) by injecting resources and runtime resource constraints (RRCs) into the specification. Resources are mandatory for executing the time points and their availability is represented through temporal expressions, whereas RRCs restrict resource availability by further temporal constraints among resources. We provide a fully-automated encoding to translate any CSTNUR into an equivalent timed game automaton in polynomial time for a sound and complete DC-checking.

The workflow satisfiability problem is the problem of finding an assignment of users to tasks (i.e., a plan) so that all authorization constraints are satisfied. The workflow resiliency problem is a dynamic workflow satisfiability problem coping with the absence of users. If a workflow is resilient, it is of course satisfiable, but the vice versa does not hold. There are three levels of resiliency: in static resiliency, up to k users might be absent before the execution starts and never become available for that execution; in decremental resiliency, up to k users might be absent before or during execution and, again, they never become available for that execution; in dynamic resiliency, up to k users might be absent before executing any task and they may in general turn absent and available continuously, before or during the execution. Much work has been carried out to address static resiliency, little for decremental resiliency and, to the best of our knowledge, for dynamic resiliency no exact approach that returns a dynamic execution plan if and only if a workflow is resilient has been provided so far. In this paper, we tackle workflow resiliency via extended game automata. We provide three encodings (having polynomial-time complexity) from workflows to extended game automata to model each kind of resiliency as an instantaneous game and we use Uppaal-TIGA to synthesize a winning strategy (i.e., a controller) for such a game. If a controller exists, then the workflow is resilient (as the controller’s strategy corresponds to a dynamic plan). If it doesn’t, then the workflow is breakable. The approach that we propose is correct because it corresponds to a reachability problem for extended game automata (TCTL model checking). Moreover, we have developed Erre, the first tool for workflow resiliency that relies on a controller synthesis approach for the three kinds of resiliency. Thanks to Erre, our approach is thus also fully-automated from analysis to simulation.

The formal specification of privacy goals in symbolic protocol models has proved to be not quite trivial so far. The most widely used approach in formal methods is based on the static equivalence of frames in the applied pi-calculus, basically asking whether or not the intruder is able to distinguish two given worlds. But then a subtle question emerges: How can we be sure that we have specified all pairs of worlds to properly reflect our intuitive privacy goal? To address this problem, we introduce in this article a novel and declarative way to specify privacy goals, called (α, β)-privacy. This new approach is based on specifying two formulae α and β in first-order logic with Herbrand universes, where α reflects the intentionally released information and β includes the actual cryptographic (“technical”) messages the intruder can see. Then (α, β)-privacy means that the intruder cannot derive any “nontechnical” statement from β that he cannot derive from α already. We describe by a variety of examples how this notion can be used in practice. Even though (α, β)-privacy does not directly contain a notion of distinguishing between worlds, there is a close relationship to static equivalence of frames that we investigate formally. This allows us to justify (and criticize) the specifications that are currently used in verification tools and obtain a decision procedure for a large fragment of (α, β)-privacy.

Constraint Networks (CNs) are a framework to model the constraint satisfaction problem (CSP), which is the problem of finding an assignment of values to a set of variables satisfying a set of given constraints. Therefore, CSP is a satisfiability problem. When the CSP turns conditional, consistency analysis extends to finding also an assignment to these conditions such that the relevant part of the initial CN is consistent. However, CNs fail to model CSPs expressing an uncontrollable conditional part (i.e., a conditional part that cannot be decided but merely observed as it occurs). To bridge this gap, in this paper we propose constraint networks under conditional uncertainty (CNCUs), and we define weak, strong and dynamic controllability of a CNCU. We provide algorithms to check each of these types of controllability and discuss how to synthesize (dynamic) execution strategies that drive the execution of a CNCU saying which value to assign to which variable depending on how the uncontrollable part behaves. We benchmark the approach by using ZETA, a tool that we developed for CNCUs. What we propose is fully automated from analysis to simulation.

Temporal role-based access control models support the specification and enforcement of several temporal constraints on role enabling, role activation, and temporal role hierarchies among others. In this paper, we define three mappings that preserve the solutions to a class of policy problems: they map security analysis problems in presence of static temporal role hierarchies to problems without them. We show how our mappings can be used to extend the capabilities of a tool for the analysis of administrative temporal role-based access control policies to reason in presence of temporal role hierarchies. We carried out an experimental evaluation with a prototype implementation, which highlighted that one of the proposed mappings behaves better than the other two. To the best of our knowledge, ours is the first tool capable of reasoning with (static) temporal role hierarchies.

Summary Web applications have become one of the preferred means for users to perform a number of crucial and security‐sensitive operations such as selling and buying goods or managing bank accounts, official documents, personal health records, and smart houses. The pervasive adoption of such web applications calls for an extensive security analysis in order to avoid attacks. Penetration testing is the most common approach for testing the security of web applications, but model‐based security testing has been steadily maturing into a viable alternative and/or complementary approach. Penetration testing is very efficient, but the experience of the security analyst is crucial; model‐based security testing relies on formal methods, but the security analyst has to first create a suitable model of the web application. In this paper, we introduce MobSTer, a formal and flexible model‐based security testing framework that contributes to filling the gap between these two security testing approaches. The main idea underlying this framework is that the use of model‐checking techniques can automate the search for possible vulnerable entry points in the web application, ie, it permits an analyst to perform security testing without missing important checks. Moreover, the framework also allows for reuse: The analyst can collect her expertise into the framework and (re)use it during future tests on possibly different web applications. We have implemented MobSTer as a prototype and applied it to test a number of case studies to assess its strength and concretely evaluate it with respect to four state‐of‐the‐art tools normally used by penetration testers.

We apply formal methods to lay and streamline theoretical foundations to reason about Cyber-Physical Systems (CPSs) and cyber-physical attacks. We focus on integrity and DoS attacks to sensors and actuators of CPSs, and on the timing aspects of these attacks. Our contributions are threefold: (1) we define a hybrid process calculus to model both CPSs and cyber-physical attacks. (2) we define a threat model of cyber-physical attacks and 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. We illustrate definitions and results by means of a non-trivial engineering application.

We define Access-Controlled Temporal Networks (ACTNs) as an extension of Conditional Simple Temporal Networks with Uncertainty (CSTNUs). CSTNUs are able to handle features such as contingent durations and conditional constraints, and have thus been used to model the temporal constraints of workflows underlying business processes. However, CSTNUs are unable to model users and authorization constraints, and thus cannot model "who can do what, when". ACTNs solve this problem by adding users and authorization constraints that must be considered together with temporal constraints. Dynamic controllability (DC) of ACTNs ensures the existence of an execution strategy, able to assign tasks to authorized users dynamically, satisfying all the relevant authorization constraints no matter what contingent durations turn out to be or what conditional constraints have to be considered. We show that the DC checking can be done via Timed Game Automata and provide experimental results using UPPAAL-TIGA on a concrete real-world case study.

Interpolation has been successfully applied in formal methods for model checking and test-case generation for sequential programs. Security protocols, however, exhibit idiosyncrasies that make them unsuitable for the direct application of interpolation. We address this problem and present an interp olation-based method for security protocol verification. Our method starts from a protocol specification and combines Craig interpolation, symbolic execution and the standard Dolev–Yao intruder model to search for possible attacks on the protocol. Interpolants are generated as a response to search failure in order to prune possible useless traces and speed up the exploration. We illustrate our method by means of concrete examples and discuss the results obtained by using a prototype implementation.

TEST 02 - Elsevier's Scopus, the largest abstract and citation database of peer-reviewed literature. Search and access research from the science, technology, medicine, social sciences and arts and humanities fields.

Vertical composition of security protocols means that an application protocol (e.g., a banking service) runs over a channel established by another protocol (e.g., a secure channel provided by TLS). This naturally gives rise to a compositionality question: given a secure protocol P1 that provides a certain kind of channel as a goal and another secure protocol P2 that assumes this kind of channel, can we then derive that their vertical composition P2[P1] is secure? It is well known that protocol composition can lead to attacks even when the individual protocols are all secure in isolation. In this paper, we formalize seven easy-to-check static conditions that support a large class of channels and applications and that we prove to be sufficient for vertical security protocol composition.

In many real-life situations making a decision entails evaluating the risks associated with the decision, which in turn requires reasoning about events and their relations. In addition to the simpler and better-understood notions of causation and precondition, in this paper we focus on block (or prevention), which is the relation established between an event φ1and another event φ2such that the number of occurrences of φ2decreases whenever φ1occurs, and mitigation, where the occurrence of φ1reduces the “negative” (for the particular decision we are considering) consequences of the occurrence of φ2. By introducing two further counting operators and the notion of interval of observation, we give here a sound and complete tableau system along with a systematic tableau construction procedure.

We describe the SPaCIoS project, illustrating its main objectives, the results obtained so far and those that we expect to achieve, in particular, the development of the SPaCIoS Tool, an integrated platform that takes as input a formal description of the system under validation, the expected security goals, and a description of the capabilities of the attacker, and automatically generates and executes a sequence of test cases on the system through a number of proxies.

We propose an approach for defining labeled natural deduction systems for the class of Peircean branching temporal logics, seen as logics in their own right rather than as sub logics of Ockhamist systems. In particular, we give a system for the logic UB, i.e., the until-free fragment of CTL, and show that it is sound and complete. We also study normalization and discuss how derivations may reduce to a normal form using an appropriate management of proof contexts. Finally, we briefly discuss how to extend our system in order to capture full CTL.

Although computer security typically revolves around threats, attacks and defenses, the sub-field of security protocol analysis (SPA) has so far focused almost exclusively on attacks. In this paper, we show that such focus on attacks depends on few critical assumptions that have been characteristic

Security-sensitive business processes are business processes that must comply with security requirements such as authorization constraints or separation or binding of duty. As such, they are difficult to design and notoriously prone to error, and a number of approaches have been proposed to formalizing and reasoning about models of such processes to detect potential vulnerabilities. In this paper, we present an approach that introduces the notion of knowledge for the formal analysis of security-sensitive business processes. We structure knowledge hierarchically, in different levels that can interact with each other in order to derive new information, which allows us to specify at different levels information about sets of critical tasks and thereby control the process execution and enforce security properties.

We give a sound and complete labelled natural deduction system for a bundled branching temporal logic, namely the until-free version of BCTL*. The logic BCTL* is obtained by referring to a more general semantics than that of CTL*, where we only require that the set of paths in a model is closed under taking suffixes (i.e. is suffix-closed) and is closed under putting together a finite prefix of one path with the suffix of any other path beginning at the same state where the prefix ends (i.e. is fusion-closed). In other words, this logic does not enjoy the so-called limit-closure property of the standard CTL* validity semantics. We give both a classical and an intuitionistic version of our labelled natural deduction system for the until-free version of BCTL*, and carry out a proof-theoretical analysis of the intuitionistic system: we prove that derivations reduce to a normal form, which allows us to give a purely syntactical proof of consistency (for both the intuitionistic and classical versions) of the deduction system.

Several different secure routing protocols have been proposed for determining the appropriate paths on which data should be transmitted in ad hoc networks. In this paper, we focus on two of the most relevant such protocols, ARAN and end air A, and present the results of a formal analysis that we have carried out using the AVISPA Tool, an automated model checker for the analysis of security protocols. By model checking ARAN with the AVISPA Tool, we have discovered three attacks (a route disruption, a route diversion, and a creation of incorrect routing state), while our analysis of end air A revealed no attacks.

We introduce constraint differentiation, a powerful technique for reducing search when model-checking security protocols using constraint-based methods. Constraint differentiation works by eliminating certain kinds of redundancies that arise in the search space when using constraints to represent a nd manipulate the messages that may be sent by an active intruder. We define constraint differentiation in a general way, independent of the technical and conceptual details of the underlying constraint-based method and protocol model. Formally, we prove that constraint differentiation terminates and is correct, under the assumption that the original constraint-based approach has these properties. Practically, as a concrete case study, we have integrated this technique into OFMC, a state-of-the-art model-checker for security protocol analysis, and demonstrated its effectiveness by extensive experimentation. Our results show that constraint differentiation substantially reduces search and considerably improves the performance of OFMC, enabling its application to a wider class of problems.

The distributed temporal logic DTL is a logic for reasoning about temporal properties of discrete distributed systems from the local point of view of the system's agents, which are assumed to execute sequentially and to interact by means of synchronous event sharing. We present a sound and complete labelled tableaux system for full DTL. To achieve this, we first formalize a labelled tableaux system for reasoning locally at each agent and afterwards we combine the local systems into a global one by adding rules that capture the distributed nature of DTL. We also provide examples illustrating the use of DTL and our tableaux system.

DTL is a distributed temporal logic for reasoning about temporal properties of distributed systems from the local point of view of the system's agents, which are assumed to execute sequentially and to interact by means of synchronous event sharing. We present a sound and complete labeled tableaux system for future-time DTL. To achieve this, we first formalize a labeled tableaux system for reasoning locally at each agent, which provides a system for full future-time LTL, and afterwards we combine the local systems into a global one by adding rules that capture the distributed nature of DTL.

We give labeled natural deduction systems for a family of tense logics extending the basic linear tense logic Kl. We prove that our systems are sound and complete with respect to the usual Kripke semantics, and that they possess a number of useful normalization properties (in particular, derivations reduce to a normal form that enjoys a subformula property). We also discuss how to extend our systems to capture richer logics like (fragments of) LTL.

We introduce CDiff, a new technique for reducing search when model-checking security protocols. Our technique is based on eliminating certain kinds of redundancies that arise in the search space when using symbolic exploration methods, in particular methods that employ constraints to represent and manipulate possible messages from an active intruder. Formally, we prove that CDiff terminates and is correct and complete, in that it preserves the set of reachable states so that all state-based properties holding before reduction (such as the intruder discovering a secret on the network) hold after reduction. Practically, we have integrated this technique into OFMC, a state-of-the-art model-checker, and demonstrated its effectiveness by extensive experimentation. Our results show that CDiff substantially reduces search and considerably improves the performance of OFMC, enabling its application to a wider class of problems.

We give a categorial characterization of how labelled deduction systems for logics with a propositional basis behave under unconstrained fibring and under fibring that is constrained by symbol sharing. At the semantic level, we introduce a general semantics for our systems and then give a categorial characterization of fibring of models. Based on this, we establish the conditions under which our systems are sound and complete with respect to the general semantics for the corresponding logics, and establish requirements on logics and systems so that completeness is preserved by both forms of fibring.

We use the formal language Z to specify and analyze the security service of CORBA. In doing so, we tackle the problem of how one can apply lightweight formal methods to improve the precision and aid the analysis of a substantial, informal specification. Our approach is scenario-driven: we use representative scenarios to determine which parts of the informal specification should be formalized and then verify the formal specification against the requirements of these scenarios.

We show how labelled deductive systems can be combined with a logical framework to provide a natural deduction implementation of a large and well-known class of propositional modal logics (including K, D, T, B, S4, S4.2, KD45, S5). Our approach is modular and based on a separation between a base logic and a labelling algebra, which interact through a fixed interface. While the base logic stays fixed, different modal logics are generated by plugging in appropriate algebras. This leads to a hierarchical structuring of modal logics with inheritance of theorems. Moreover, it allows modular correctness proofs, both with respect to soundness and completeness for semantics, and faithfulness and adequacy of the implementation. We also investigate the tradeoffs in possible labelled presentations: we show that a narrow interface between the base logic and the labelling algebra supports modularity and provides an attractive proof-theory but limits the degree to which we can make use of extensions to the labelling algebra.