YAPA: A Generic Tool for Computing Intruder Knowledge

DOI10.1007/978-3-642-02348-4_11MaRDI QIDQ3636824zbMATH OpenOpenAlexFDO

Authors Mathieu Baudet, Véronique Cortier, Stéphanie Delaune

Publication date 30 June 2009

Published in Rewriting Techniques and Applications (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Data encryption (aspects in computer science) (68P25) Grammars and rewriting systems (68Q42) Cryptography (94A60)

Abstract: Reasoning about the knowledge of an attacker is a necessary step in many formal analyses of security protocols. In the framework of the applied pi calculus, as in similar languages based on equational logics, knowledge is typically expressed by two relations: deducibility and static equivalence. Several decision procedures have been proposed for these relations under a variety of equational theories. However, each theory has its particular algorithm, and none has been implemented so far. We provide a generic procedure for deducibility and static equivalence that takes as input any convergent rewrite system. We show that our algorithm covers most of the existing decision procedures for convergent theories. We also provide an efficient implementation, and compare it briefly with the tools ProVerif and KiSs.

Recommendations

• YAPA: a generic tool for computing intruder knowledge
• Computing knowledge in security protocols under convergent equational theories
• Computing Knowledge in Security Protocols under Convergent Equational Theories
• Automata, Languages and Programming
• Computing knowledge in equational extensions of subterm convergent theories

Cites work

• An NP decision procedure for protocol insecurity with XOR
• Analysing password protocol security against off-line dictionary attacks
• Automata, Languages and Programming
• Automated verification of selected equivalences for security protocols
• Deciding Knowledge in Security Protocols for Monoidal Equational Theories
• Deciding knowledge in security protocols under equational theories
• Foundations of Software Science and Computation Structures
• Intruders with Caps
• Mobile values, new names, and secure communication
• Verifying privacy-type properties of electronic voting protocols: a taster
• YAPA: a generic tool for computing intruder knowledge

Cited in

(12)

• YAPA
• YAPA: a generic tool for computing intruder knowledge
• Deciding knowledge in security protocols under some e-voting theories
• Model Checking Security Protocols
• Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties
• Reducing equational theories for the decision of static equivalence
• Computing knowledge in security protocols under convergent equational theories
• Computing Knowledge in Security Protocols under Convergent Equational Theories
• Automated verification of equivalence properties of cryptographic protocols
• FAST: an efficient decision procedure for deduction and static equivalence
• Automating security analysis: symbolic equivalence of constraint systems
• Compiling and securing cryptographic protocols

Describes a project that uses

Uses Software

• ProVerif
• AVISPA

This page was built for publication: YAPA: A Generic Tool for Computing Intruder Knowledge

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