Dynamic tags for security protocols

DOI10.2168/LMCS-10(2:11)2014zbMATH Open1315.94050arXiv1405.2738WikidataQ114952761 ScholiaQ114952761MaRDI QIDQ4979449FDOQ4979449

Authors: Myrto Arapinis, Stéphanie Delaune, Steve Kremer 

Publication date: 23 June 2014

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Abstract: The design and verification of cryptographic protocols is a notoriously difficult task, even in symbolic models which take an abstract view of cryptography. This is mainly due to the fact that protocols may interact with an arbitrary attacker which yields a verification problem that has several sources of unboundedness (size of messages, number of sessions, etc. In this paper, we characterize a class of protocols for which deciding security for an unbounded number of sessions is decidable. More precisely, we present a simple transformation which maps a protocol that is secure for a bounded number of protocol sessions (a decidable problem) to a protocol that is secure for an unbounded number of sessions. The precise number of sessions that need to be considered is a function of the security property and we show that for several classical security properties a single session is sufficient. Therefore, in many cases our results yields a design strategy for security protocols: (i) design a protocol intended to be secure for a {single session}; and (ii) apply our transformation to obtain a protocol which is secure for an unbounded number of sessions.

Full work available at URL: https://arxiv.org/abs/1405.2738

Recommendations

• From One Session to Many: Dynamic Tags for Security Protocols
• Protocol Security and Algebraic Properties: Decision Results for a Bounded Number of Sessions
• FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science
• Bounding messages for free in security protocols -- extension to various security properties
• A (restricted) quantifier elimination for security protocols

zbMATH Keywords

formal methodsverification of cryptographic protocols

Mathematics Subject Classification ID

Data encryption (aspects in computer science) (68P25) Cryptography (94A60) Specification and verification (program logics, model checking, etc.) (68Q60) Network protocols (68M12)

Cited In (8)

• Secure composition of protocols
• Computer Science Logic
• A (restricted) quantifier elimination for security protocols
• Sessions and separability in security protocols
• Bounding Messages for Free in Security Protocols
• From One Session to Many: Dynamic Tags for Security Protocols
• Bounding messages for free in security protocols -- extension to various security properties
• Title not available (Why is that?)

Uses Software

• AVISPA

This page was built for publication: Dynamic tags for security protocols

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4979449)