Compiling and securing cryptographic protocols

DOI10.1016/J.IPL.2009.11.004MaRDI QIDQ990127zbMATH OpenOpenAlexFDO

Authors Yannick Chevalier, Michaël Rusinowitch

Publication date 2 September 2010

Published in Information Processing Letters (Search for Journal in Brave)

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

zbMATH Keywords

formal methodssafety/security in digital systemscryptographic protocolsrolesDolev Yao modelprotocol compiling

Mathematics Subject Classification ID

Data encryption (aspects in computer science) (68P25)

Abstract: Protocol narrations are widely used in security as semi-formal notations to specify conversations between roles. We define a translation from a protocol narration to the sequences of operations to be performed by each role. Unlike previous works, we reduce this compilation process to well-known decision problems in formal protocol analysis. This allows one to define a natural notion of prudent translation and to reuse many known results from the literature in order to cover more crypto-primitives. In particular this work is the first one to show how to compile protocols parameterised by the properties of the available operations.

Recommendations

• A formal semantics for protocol narrations
• Trustworthy Global Computing
• scientific article; zbMATH DE number 1696763
• scientific article; zbMATH DE number 3965967
• The practice of cryptographic protocol verification

Cites work

• scientific article; zbMATH DE number 1696763 (Why is no real title available?)
• Automata, Languages and Programming
• Combining Algorithms for Deciding Knowledge in Security Protocols
• Compiling and securing cryptographic protocols
• Cryptographic Protocol Explication and End-Point Projection
• Deciding Knowledge in Security Protocols for Monoidal Equational Theories
• Deciding knowledge in security protocols under equational theories
• Intruders with Caps
• On the semantics of Alice \& Bob specifications of security protocols
• Using encryption for authentication in large networks of computers
• YAPA: A Generic Tool for Computing Intruder Knowledge

Cited in

(8)

• Decidability of equivalence of symbolic derivations
• scientific article; zbMATH DE number 1696763 (Why is no real title available?)
• Alice and Bob meet equational theories
• A formal semantics for protocol narrations
• Compiling and securing cryptographic protocols
• Alice and Bob: reconciling formal models and implementation
• Trustworthy Global Computing
• Proved generation of implementations from computationally secure protocol specifications

Describes a project that uses

Uses Software

• Casper
• YAPA

This page was built for publication: Compiling and securing cryptographic protocols

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