Standard
An experiment in ping-pong protocol verification by nondeterministic pushdown automata. / Glück, Robert.
Proceedings Third Workshop on Models for Formal Analysis of Real Systems and Sixth International Workshop on Verification and Program Transformation. Proceedings. red. / John P. Gallagher; Rob van Glabbeek; Wendelin Serwe. Open Publishing Association, 2018. s. 169-184 (Electronic Proceedings in Theoretical Computer Science, Bind 268).
Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › fagfællebedømt
Harvard
Glück, R 2018,
An experiment in ping-pong protocol verification by nondeterministic pushdown automata. i JP Gallagher, R van Glabbeek & W Serwe (red),
Proceedings Third Workshop on Models for Formal Analysis of Real Systems and Sixth International Workshop on Verification and Program Transformation. Proceedings. Open Publishing Association, Electronic Proceedings in Theoretical Computer Science, bind 268, s. 169-184, 6th International Workshop on Verification and Program Transformation, Thessaloniki, Grækenland,
20/04/2018.
https://doi.org/10.4204/EPTCS.268.6
APA
Glück, R. (2018).
An experiment in ping-pong protocol verification by nondeterministic pushdown automata. I J. P. Gallagher, R. van Glabbeek, & W. Serwe (red.),
Proceedings Third Workshop on Models for Formal Analysis of Real Systems and Sixth International Workshop on Verification and Program Transformation. Proceedings (s. 169-184). Open Publishing Association. Electronic Proceedings in Theoretical Computer Science Bind 268
https://doi.org/10.4204/EPTCS.268.6
Vancouver
Glück R.
An experiment in ping-pong protocol verification by nondeterministic pushdown automata. I Gallagher JP, van Glabbeek R, Serwe W, red., Proceedings Third Workshop on Models for Formal Analysis of Real Systems and Sixth International Workshop on Verification and Program Transformation. Proceedings. Open Publishing Association. 2018. s. 169-184. (Electronic Proceedings in Theoretical Computer Science, Bind 268).
https://doi.org/10.4204/EPTCS.268.6
Author
Glück, Robert. / An experiment in ping-pong protocol verification by nondeterministic pushdown automata. Proceedings Third Workshop on Models for Formal Analysis of Real Systems and Sixth International Workshop on Verification and Program Transformation. Proceedings. red. / John P. Gallagher ; Rob van Glabbeek ; Wendelin Serwe. Open Publishing Association, 2018. s. 169-184 (Electronic Proceedings in Theoretical Computer Science, Bind 268).
Bibtex
@inproceedings{b02b9eb8ab934726b036e157065c2760,
title = "An experiment in ping-pong protocol verification by nondeterministic pushdown automata",
abstract = "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.",
author = "Robert Gl{\"u}ck",
year = "2018",
doi = "10.4204/EPTCS.268.6",
language = "English",
series = "Electronic Proceedings in Theoretical Computer Science",
publisher = "Open Publishing Association",
pages = "169--184",
editor = "Gallagher, {John P.} and {van Glabbeek}, Rob and Wendelin Serwe",
booktitle = "Proceedings Third Workshop on Models for Formal Analysis of Real Systems and Sixth International Workshop on Verification and Program Transformation. Proceedings",
note = "6th International Workshop on Verification and Program Transformation, VPT 18 ; Conference date: 20-04-2018",
}
RIS
TY - GEN
T1 - An experiment in ping-pong protocol verification by nondeterministic pushdown automata
AU - Glück, Robert
PY - 2018
Y1 - 2018
N2 - 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.
AB - 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.
U2 - 10.4204/EPTCS.268.6
DO - 10.4204/EPTCS.268.6
M3 - Article in proceedings
T3 - Electronic Proceedings in Theoretical Computer Science
SP - 169
EP - 184
BT - Proceedings Third Workshop on Models for Formal Analysis of Real Systems and Sixth International Workshop on Verification and Program Transformation. Proceedings
A2 - Gallagher, John P.
A2 - van Glabbeek, Rob
A2 - Serwe, Wendelin
PB - Open Publishing Association
T2 - 6th International Workshop on Verification and Program Transformation
Y2 - 20 April 2018
ER -
