Joseph Y. Halpern ; Riccardo Pucella - Modeling Adversaries in a Logic for Security Protocol Analysis

lmcs:688 - Logical Methods in Computer Science, March 9, 2012, Volume 8, Issue 1 - https://doi.org/10.2168/LMCS-8(1:21)2012
Modeling Adversaries in a Logic for Security Protocol AnalysisArticle

Authors: Joseph Y. Halpern ; Riccardo Pucella

    Logics for security protocol analysis require the formalization of an adversary model that specifies the capabilities of adversaries. A common model is the Dolev-Yao model, which considers only adversaries that can compose and replay messages, and decipher them with known keys. The Dolev-Yao model is a useful abstraction, but it suffers from some drawbacks: it cannot handle the adversary knowing protocol-specific information, and it cannot handle probabilistic notions, such as the adversary attempting to guess the keys. We show how we can analyze security protocols under different adversary models by using a logic with a notion of algorithmic knowledge. Roughly speaking, adversaries are assumed to use algorithms to compute their knowledge; adversary capabilities are captured by suitable restrictions on the algorithms used. We show how we can model the standard Dolev-Yao adversary in this setting, and how we can capture more general capabilities including protocol-specific knowledge and guesses.


    Volume: Volume 8, Issue 1
    Published on: March 9, 2012
    Imported on: November 9, 2010
    Keywords: Computer Science - Cryptography and Security,Computer Science - Logic in Computer Science,cs.LO
    Funding:
      Source : OpenAIRE Graph
    • Foundations of XML - Safe Processing of Dynamic Data over the Internet; Funder: European Commission; Code: 233599
    • Towards Improved Logics For Reasoning About Security; Funder: National Science Foundation; Code: 0208535

    2 Documents citing this article

    Consultation statistics

    This page has been seen 1430 times.
    This article's PDF has been downloaded 429 times.