An experiment in ping-pong protocol verification by nondeterministic pushdown automata
Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › fagfællebedømt
Dokumenter
- An experiment in ping-pong protocol
Forlagets udgivne version, 189 KB, PDF-dokument
An experiment is described that confirms the security of a well-studied class of cryptographic protocols(Dolev-Yao intruder model) can be verified by two-way nondeterministic pushdown automata(2NPDA). A nondeterministic pushdown program checks whether the intersection of a regular language(the protocol to verify) and a given Dyck language containing all canceling words is empty. Ifit is not, an intruder can reveal secret messages sent between trusted users. The verification is guaranteedto terminate in cubic time at most on a 2NPDA-simulator. The interpretive approach used in thisexperiment simplifies the verification, by separating the nondeterministic pushdown logic and programcontrol, and makes it more predictable. We describe the interpretive approach and the knowntransformational solutions, and show they share interesting features. Also noteworthy is how abstractresults from automata theory can solve practical problems by programming language means.
Originalsprog | Engelsk |
---|---|
Titel | Proceedings Third Workshop on Models for Formal Analysis of Real Systems and Sixth International Workshop on Verification and Program Transformation. Proceedings |
Redaktører | John P. Gallagher, Rob van Glabbeek, Wendelin Serwe |
Forlag | Open Publishing Association |
Publikationsdato | 2018 |
Sider | 169-184 |
DOI | |
Status | Udgivet - 2018 |
Begivenhed | 6th International Workshop on Verification and Program Transformation - Thessaloniki, Grækenland Varighed: 20 apr. 2018 → … |
Workshop
Workshop | 6th International Workshop on Verification and Program Transformation |
---|---|
Land | Grækenland |
By | Thessaloniki |
Periode | 20/04/2018 → … |
Navn | Electronic Proceedings in Theoretical Computer Science |
---|---|
Vol/bind | 268 |
ISSN | 2075-2180 |
Antal downloads er baseret på statistik fra Google Scholar og www.ku.dk
Ingen data tilgængelig
ID: 194063040