1,721,151 research outputs found
A Recipe for the Complexity Analysis of Non-Classical Logics
No full textIn previous work, we introduced a framework for the uniform formalization of families of non-classical logics with Kripke semantics, such as modal and relevance logics. Here we show how to use this framework to analyze the complexity of the decision problem for these logics, also in a uniform way. The result is a recipe: the user contributes bounds on structural reasoning and the accessibility relation associated with the Kripke semantics and the result is a decision procedure with bounded space requirements. As examples, we give PSPACE decision procedures for the modal logics K4 and S4, and for a positive fragment of the relevance logic B
On the semantics of Alice&Bob specifications of security protocols
No full textIn the context of security protocols, the so-called Alice&Bob notation is often used to describe the messages exchanged between honest principals in successful protocol runs. While intuitive, this notation is ambiguous in its description of the actions taken by principals, in particular with respect to the conditions they must check when executing their roles and the actions they must take when the checks fail.
In this paper, we investigate the semantics of protocol specifications in Alice&Bob notation. We provide both a denotational and an operational semantics for such specifications, rigorously accounting for these conditions and actions. Our denotational semantics is based on a notion of incremental symbolic runs, which reflect the data possessed by principals and how this data increases monotonically during protocol execution. We contrast this with a standard formalization of the behavior of principals, which directly interprets message exchanges as sequences of atomic actions. In particular, we provide a complete characterization of the situations where this simpler, direct approach is adequate and prove that incremental symbolic runs are more expressive in general. Our operational semantics, which is guided by the denotational semantics, implements each role of the specified protocol as a sequential process of the pattern-matching spi calculus
Deconstructing Alice and Bob
No full textAlice&Bob–notation is a simple notation for describing security protocols as sequences of message exchanges. We show that, despite the fact that Alice&Bob–notation does not include explicit control flow constructs, it is possible to make some of these aspects explicit when producing formal protocol models without having to resort to more expressive protocol description languages. We introduce a notion of incremental symbolic run to formally handle message forwarding and conditional abortion. In incremental symbolic runs, we use variables to represent messages that the principals cannot read, and we characterize each of the execution steps in order to build a collection of symbolic subruns of increasing lengths, reflecting the data possessed by the principals up to that point in the execution. We contrast this with the simpler (more standard) approach based on formalizing the behavior of principals by directly interpreting message exchanges as sequences of atomic actions. In particular, we provide a complete characterization of the situations where this simpler approach is adequate and prove that incremental symbolic runs are more expressive in general
Metareasoning about Security Protocols using Distributed Temporal Logic
No full textWe introduce a version of distributed temporal logic for rigorously formalizing and proving metalevel properties of different protocol models, and establishing relationships between models. The resulting logic is quite expressive and provides a natural, intuitive language for formalizing both local (agent specific) and global properties of distributed communicating processes. Through a sequence of examples, we show how this logic may be applied to formalize and establish the correctness of different modeling and simplification techniques, which play a role in building effective protocol tools
Modal logics K, T, K4, S4: labelled proof systems and new complexity results
No full textModal logics K, T, K4, S4: labelled proof systems and new complexity result
Relating Strand Spaces and Distributed Temporal Logic for Security Protocol Analysis
No full textIn previous work, we introduced a version of distributed temporal logic that is well-suited both for verifying security protocols and as a metalogic for reasoning about, and relating, different security protocol models. In this paper, we formally investigate the relationship between our approach and strand spaces, which is one of the most successful and widespread formalisms for analyzing security protocols. We define translations between models in our logic and strand-space models of security protocols, and we compare the results obtained with respect to the level of abstraction that is inherent in each of the formalisms. This allows us to clarify different aspects of strand spaces that are often left implicit, as well as pave the way to transfer results, techniques and tools across the two approaches
Towards an awareness-based semantics for security protocol analysis
No full textWe report on work-in-progress on a new semantics for analyzing security protocols that combines complementary features of security logics and inductive methods. We use awareness to model the agents' resource-bounded reasoning and, in doing so, capture a more appropriate notion of belief than those usually considered in security logics. We also address the problem of modeling interleaved protocol executions, adapting ideas from inductive methods for protocol verification. The result is an intuitive, but expressive, doxastic logic for formalizing and reasoning about attacks. As a case study, we use awareness to characterize, and demonstrate the existence of, a man-in-the-middle attack upon the Needham-Schroeder Public Key protocol. This is, to our knowledge, not only the first doxastic analysis of this attack but also the first practical application of an awareness logic. Even though defining the awareness sets of the agents, a task that is left unspecified in formal works on awareness logics, turns out to be surprisingly subtle, initial results suggest that our approach is promising for modeling, verifying and reasoning about security protocols and their properties
Modal Specifications of Trace-Based Security Properties
No full textWe introduce a multi-modal logic that combines complementary features of authentication logics and trace-based approaches. Our logic contains two kinds of modalities: implicit belief, which formalizes the view of an external agent reasoning about interleaved protocol executions, and explicit belief, which uses awareness to model the resource-bounded reasoning of the agents involved in the executions. We employ these modalities to formalize extensional and intensional specifications of protocols and their properties, and use these formalizations to characterize and reason about attacks. As an example, we consider the Needham-Schroeder Public Key protocol and use our logic to demonstrate the existence of the well-known man-in-the-middle attack, and also show the equivalence of our modal specification to one based on an interleaved trace semantics
Constraint Differentiation: A New Reduction Technique for Constraint-Based Analysis of Security Protocols (Extended Abstract)
No full textConstraint Differentiation: A New Reduction Technique for Constraint-Based Analysis of Security Protocols (Extended Abstract
Special Issue of the Journal of Automated Reasoning on "Automated Reasoning for Security Protocol Analysis"
No full text- …
