A procedure for deciding symbolic equivalence between sets of constraint systems

DOI10.1016/J.IC.2017.05.004MaRDI QIDQ2013557zbMATH OpenOpenAlexFDO

Authors Vincent Cheval, Hubert Comon-Lundh, Stéphanie Delaune

Publication date 8 August 2017

Published in Information and Computation (Search for Journal in Brave)

Full work available at URL https://kar.kent.ac.uk/46882/1/CDD-IC-submitted.pdf

zbMATH Keywords

verificationformal methodssecurity protocolssymbolic modelprivacy-type properties

Mathematics Subject Classification ID

Cryptography (94A60) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Automating security analysis: symbolic equivalence of constraint systems
• Deciding equivalence-based properties using constraint solving
• A survey of symbolic methods for establishing equivalence-based properties in cryptographic protocols
• A reduced semantics for deciding trace equivalence
• Typing messages for free in security protocols: the case of equivalence properties

Cites work

• scientific article; zbMATH DE number 1142316 (Why is no real title available?)
• A survey of symbolic methods in computational analysis of cryptographic systems
• Automated verification of equivalence properties of cryptographic protocols
• Automated verification of selected equivalences for security protocols
• Automating security analysis: symbolic equivalence of constraint systems
• Computer Aided Verification
• Decidability of equivalence of symbolic derivations
• Deciding equivalence-based properties using constraint solving
• Deciding security properties for cryptographic protocols. application to key cycles
• Equational problems and disunification
• Mobile values, new names, and secure communication
• Private authentication
• Proving more observational equivalences with ProVerif
• Term Rewriting and Applications

Cited in

(12)

• Deciding equivalence-based properties using constraint solving
• Reduction of equational theories for verification of trace equivalence: re-encryption, associativity and commutativity
• Typing messages for free in security protocols: the case of equivalence properties
• Compositional analysis of protocol equivalence in the applied \(\pi \)-calculus using quasi-open bisimilarity
• A symbolic-interval inference approach for constraint satisfaction: implementation on kinematics applications
• When privacy fails, a formula describes an attack: a complete and compositional verification method for the applied \(\pi\)-calculus
• Efficiently deciding equivalence for standard primitives and phases
• A reduced semantics for deciding trace equivalence
• Automating security analysis: symbolic equivalence of constraint systems
• Automated verification of equivalence properties of cryptographic protocols
• Rewriting Privacy
• A decision procedure for semantical equivalence of thin FM specifications

Describes a project that uses

Uses Software

• TAMARIN
• Akiss
• Apte
• scyther
• AVISPA

This page was built for publication: A procedure for deciding symbolic equivalence between sets of constraint systems

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