Compiling and securing cryptographic protocols

DOI10.1016/J.IPL.2009.11.004zbMATH Open1209.68211arXiv0910.5099OpenAlexW2030265421MaRDI QIDQ990127FDOQ990127

Authors: Yannick Chevalier, Michaël Rusinowitch 

Publication date: 2 September 2010

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

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.

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

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

zbMATH Keywords

formal methodssafety/security in digital systemscryptographic protocolsrolesDolev Yao modelprotocol compiling

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (7)

• Decidability of equivalence of symbolic derivations
• Title not available (Why is that?)
• A formal semantics for protocol narrations
• Alice and Bob Meet Equational Theories
• Compiling and securing cryptographic protocols
• Trustworthy Global Computing
• Alice and Bob: Reconciling Formal Models and Implementation

Uses Software

• YAPA
• Casper

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)