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

DOI10.1016/J.JLAMP.2016.06.001zbMATH Open1348.68084OpenAlexW2465156511MaRDI QIDQ739638FDOQ739638

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

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

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)

Cites Work

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

Cited In (3)

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

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)