{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/78502"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/78502","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Maude-PSL: a new input language for Maude-NPA","abstract":"DSpace SAF Submission Ingestion Package generated from Vireo submission #8115 on 2015-07-22 at 10:34:04","abstract_html":"DSpace SAF Submission Ingestion Package generated from Vireo submission #8115 on 2015-07-22 at 10:34:04","abstract_has_math":false,"creators":["Cholewa, Andrew Russel"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"M.S.","degree_level":"Thesis","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":[],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2015,"date_issued":"2015-07-22T22:17:46Z","date_published":"2015-07-22T22:17:46Z","updated_at":"2026-07-22T22:26:11Z","subjects":["rewriting logic","cryptography","Maude-NRL Protocol Analyzer (Maude-NPA)","domain specific programming languages","Maude","cryptographic protocol analysis","formal specification","Maude Protocol Specification Language (Maude-PSL)"],"languages":["en"],"rights":["Copyright 2015 Andrew Russel Cholewa"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/2142/78502","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:creator","label":"Author","values":["Cholewa, Andrew Russel"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2015-07-22T22:17:46Z","2015-05","2015-04-28","2015-5"]},{"key":"dc:type","label":"Dc Type","values":["text"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Computer Science"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Thesis"]},{"key":"thesis:degree_name","label":"Degree Name","values":["M.S."]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["University of Illinois at Urbana-Champaign"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["rewriting logic","cryptography","Maude-NRL Protocol Analyzer (Maude-NPA)","domain specific programming languages","Maude","cryptographic protocol analysis","formal specification","Maude Protocol Specification Language (Maude-PSL)"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2015 Andrew Russel Cholewa"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/78502"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["DSpace SAF Submission Ingestion Package generated from Vireo submission #8115 on 2015-07-22 at 10:34:04","Maude-NPA is a narrowing-based model checker for analysing cryptographic protocols in the Dolev-Yao model modulo equations. Maude-NPA is a powerful analyzer that is sound and never returns spurious counter-examples. Maude- NPA is also very flexible, providing the user great flexibility in designing his/her own custom notation. Maude-NPA also supports a large variety of equational theories (any theory possessing the finite variant property, plus dedicated al- gorithms for homomorphism and exclusive or). However, Maude-NPA relies on a strand-based notation that, while very precise, is less familiar to users of the Alice-Bob notation. Furthermore, the input language itself is rather dif- ficult to read and write. This makes Maude-NPA hard to use, and therefore a less attractive option for protocol verification despite its power. We pro- pose a new input language called the Maude Protocol Specification Language (Maude-PSL). The Maude-PSL extends the Alice-and-Bob notation with the following additional pieces of information: the interpretation each principal has for every message he/she sends and receives, the information each principal is assumed to know at the start of the protocol execution, and the information the principal should know after execution. The Maude-PSL also provides simple yet expressive syntax for specifying intruder capabilities, secrecy attacks and authentication attacks. The Maude-PSL retains the flexible, Maude-like syn- tax for specifying the operators, type structure, and algebraic properties of a protocol. The semantics of the language is defined as a rewrite theory that rewrites Maude-PSL specifications into Maude-NPA strands. This provides a formal grounding of Maude-PSL specifications in a well understood model of cryptographic protocols.","Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2015-07-22 without embargo terms","The student, Andrew Cholewa, accepted the attached license on 2015-04-27 at 09:40.","The student, Andrew Cholewa, submitted this Thesis for approval on 2015-04-27 at 09:53.","This Thesis was approved for publication on 2015-04-28 at 07:45.","Made available in DSpace on 2015-07-22T22:17:46Z (GMT). No. of bitstreams: 2 CHOLEWA-THESIS-2015.pdf: 801056 bytes, checksum: ee1f556ea8528198cff53b4e6b2b0038 (MD5) LICENSE.txt: 4211 bytes, checksum: 14e9a7a996880512ed05d5c791c74f20 (MD5) Previous issue date: 2015-04-28"]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Maude-PSL: a new input language for Maude-NPA"]}]}],"canonical_facts":{"dc:creator":["Cholewa, Andrew Russel"],"dc:date":["2015-07-22T22:17:46Z","2015-05","2015-04-28","2015-5"],"dc:description":["DSpace SAF Submission Ingestion Package generated from Vireo submission #8115 on 2015-07-22 at 10:34:04","Maude-NPA is a narrowing-based model checker for analysing cryptographic protocols in the Dolev-Yao model modulo equations. Maude-NPA is a powerful analyzer that is sound and never returns spurious counter-examples. Maude- NPA is also very flexible, providing the user great flexibility in designing his/her own custom notation. Maude-NPA also supports a large variety of equational theories (any theory possessing the finite variant property, plus dedicated al- gorithms for homomorphism and exclusive or). However, Maude-NPA relies on a strand-based notation that, while very precise, is less familiar to users of the Alice-Bob notation. Furthermore, the input language itself is rather dif- ficult to read and write. This makes Maude-NPA hard to use, and therefore a less attractive option for protocol verification despite its power. We pro- pose a new input language called the Maude Protocol Specification Language (Maude-PSL). The Maude-PSL extends the Alice-and-Bob notation with the following additional pieces of information: the interpretation each principal has for every message he/she sends and receives, the information each principal is assumed to know at the start of the protocol execution, and the information the principal should know after execution. The Maude-PSL also provides simple yet expressive syntax for specifying intruder capabilities, secrecy attacks and authentication attacks. The Maude-PSL retains the flexible, Maude-like syn- tax for specifying the operators, type structure, and algebraic properties of a protocol. The semantics of the language is defined as a rewrite theory that rewrites Maude-PSL specifications into Maude-NPA strands. This provides a formal grounding of Maude-PSL specifications in a well understood model of cryptographic protocols.","Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2015-07-22 without embargo terms","The student, Andrew Cholewa, accepted the attached license on 2015-04-27 at 09:40.","The student, Andrew Cholewa, submitted this Thesis for approval on 2015-04-27 at 09:53.","This Thesis was approved for publication on 2015-04-28 at 07:45.","Made available in DSpace on 2015-07-22T22:17:46Z (GMT). No. of bitstreams: 2 CHOLEWA-THESIS-2015.pdf: 801056 bytes, checksum: ee1f556ea8528198cff53b4e6b2b0038 (MD5) LICENSE.txt: 4211 bytes, checksum: 14e9a7a996880512ed05d5c791c74f20 (MD5) Previous issue date: 2015-04-28"],"dc:format":["application/pdf"],"dc:identifier":["http://hdl.handle.net/2142/78502"],"dc:language":["en"],"dc:rights":["Copyright 2015 Andrew Russel Cholewa"],"dc:subject":["rewriting logic","cryptography","Maude-NRL Protocol Analyzer (Maude-NPA)","domain specific programming languages","Maude","cryptographic protocol analysis","formal specification","Maude Protocol Specification Language (Maude-PSL)"],"dc:title":["Maude-PSL: a new input language for Maude-NPA"],"dc:type":["text"],"thesis:degree_discipline":["Computer Science"],"thesis:degree_level":["Thesis"],"thesis:degree_name":["M.S."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:26:11Z"}