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

DOI10.1016/j.jlamp.2016.06.001zbMath1348.68084MaRDI 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

verification; program transformation; ping-pong protocol; supercompilation; Dolev-Yao intruder model; prefix grammar

Mathematics Subject Classification ID

68P30: Coding and information theory (compaction, compression, models of communication, encoding schemes, etc.) (aspects in computer science)

68Q42: Grammars and rewriting systems

68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Uses Software

• Refal