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

DOI10.1016/j.jlamp.2016.06.001zbMath1348.68084OpenAlexW2465156511MaRDI QIDQ739638

Antonina 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

verificationprogram transformationping-pong protocolsupercompilationDolev-Yao intruder modelprefix grammar

Mathematics Subject Classification ID

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

Uses Software

• Refal

Cites Work

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

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