Ping-pong protocols as prefix grammars: modelling and verification via program transformation

DOI10.1016/J.JLAMP.2016.06.001MaRDI QIDQ739638zbMATH OpenOpenAlexFDO

Authors Antonina N. Nepeivoda

Publication date 18 August 2016

Published in Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.jlamp.2016.06.001

zbMATH Keywords

verificationping-pong protocolprogram transformationsupercompilationDolev-Yao intruder modelprefix grammar

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Coding and information theory (compaction, compression, models of communication, encoding schemes, etc.) (aspects in computer science) (68P30) Grammars and rewriting systems (68Q42)

Recommendations

• Monotonic Set-Extended Prefix Rewriting and Verification of Recursive Ping-Pong Protocols
• Defining, analysing and implementing communication protocols using attribute grammars
• Using probabilistic Kleene algebra pKA for protocol verification
• A rewriting strategy for protocol verification
• Transformational Verification of Parameterized Protocols Using Array Formulas
• Using Probabilistic Kleene Algebra for Protocol Verification
• scientific article; zbMATH DE number 702367

Cites work

• scientific article; zbMATH DE number 1251177 (Why is no real title available?)
• Communication Theory of Secrecy Systems*
• On one application of computations with oracle
• On the security of ping-pong protocols
• On the security of public key protocols
• REACHABILITY ANALYSIS IN VERIFICATION VIA SUPERCOMPILATION
• Solving Coverability Problem for Monotonic Counter Systems by Supercompilation
• The concept of a supercompiler
• Using encryption for authentication in large networks of computers
• Verification as a parameterized testing (experiments with the SCP4 supercompiler)

Cited in

(3)

• Program specialization as a tool for solving word equations
• Decidability issues for extended ping-pong protocols
• Monotonic Set-Extended Prefix Rewriting and Verification of Recursive Ping-Pong Protocols

Describes a project that uses

Uses Software

• Refal

This page was built for publication: Ping-pong protocols as prefix grammars: modelling and verification via program transformation

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