Author name cluster

Sebastian Mödersheim

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

4 papers

2 author rows

LPAR Conference 2013 Conference Paper

Defining Privacy Is Supposed to Be Easy

Sebastian Mödersheim
Thomas Groß 0001
Luca Viganò 0001

Abstract Formally specifying privacy goals is not trivial. 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. A subtle question is how we can 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 paper a novel and declarative way to specify privacy goals, called α - β privacy, and relate it to static equivalence. 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 “non-technical” 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 partial tool support for α - β privacy.

Details

I&C Journal 2008 Journal Article

On the relationships between models in protocol verification

Sebastian Mödersheim

We formally investigate the relationships between several models that are widely used in protocol verification, namely variants of the inductive model of message traces inspired by Paulson’s approach, and models based on rewriting. More precisely, we prove several over-approximation relationships between models, i. e. that one model allows strictly more traces or reachable states than the other. This is common in verification: often an over-approximation is easier to prove correct than the original model, and proving that the over-approximation is safe implies that the original model is safe—provided that the models are indeed in an over-approximation relation. We then show that some over-approximations are not sound with respect to a common formalization of authentication goals based on exchanged messages. The precise formal account that we give on the relation of the models allows us to correct the situation.

Details DOI

LPAR Conference 2005 Conference Paper

Algebraic Intruder Deductions

David A. Basin
Sebastian Mödersheim
Luca Viganò 0001

Abstract Many security protocols fundamentally depend on the algebraic properties of cryptographic operators. It is however difficult to handle these properties when formally analyzing protocols, since basic problems like the equality of terms that represent cryptographic messages are undecidable, even for relatively simple algebraic theories. We present a framework for security protocol analysis that can handle algebraic properties of cryptographic operators in a uniform and modular way. Our framework is based on two ideas: the use of modular rewriting to formalize a generalized equational deduction problem for the Dolev-Yao intruder, and the introduction of two parameters that control the complexity of the equational unification problems that arise during protocol analysis by bounding the depth of message terms and the operations that the intruder can perform when analyzing messages. We motivate the different restrictions made in our model by highlighting different ways in which undecidability arises when incorporating algebraic properties of cryptographic operators into formal protocol analysis.

Details

LPAR Conference 2004 Conference Paper

A Formalization of Off-Line Guessing for Security Protocol Analysis

Paul Hankes Drielsma
Sebastian Mödersheim
Luca Viganò 0001

Abstract Guessing, or dictionary, attacks arise when an intruder exploits the fact that certain data like passwords may have low entropy, i. e. stem from a small set of values. In the case of off-line guessing, in particular, the intruder may employ guessed values to analyze the messages he has observed. Previous attempts at formalizing off-line guessing consist of extending a Dolev-Yao-style intruder model with inference rules to capture the additional capabilities of the intruder concerning guessable messages. While it is easy to convince oneself that the proposed rules are correct, in the sense that an intruder can actually perform such “guessing steps”, it is difficult to see whether such a system of inference rules is complete in the sense that it captures all the kinds of attacks that we would intuitively call “guessing attacks”. Moreover, the proposed systems are specialized to particular sets of cryptographic primitives and intruder capabilities. As a consequence, these systems are helpful to discover some off-line guessing attacks but are not fully appropriate for formalizing what off-line guessing precisely means and verifying that a given protocol is not vulnerable to such guessing attacks. In this paper, we give a formalization of off-line guessing by defining a deduction system that is uniform and general in that it is independent of the overall protocol model and of the details of the considered intruder model, i. e. cryptographic primitives, algebraic properties, and intruder capabilities.

Details