2026-09-20T13:50:12Z https://www.ideals.illinois.edu/oai-pmh

oai:www.ideals.illinois.edu:2142/78502 2023-07-11 col_2142_5131 col_2142_10761 com_2142_5130 com_2142_10755 com_2142_234

DSpace SAF Submission Ingestion Package generated from Vireo submission #8115 on 2015-07-22 at 10:34:04 Cholewa, Andrew Russel 2015-07-22T22:17:46Z 2015-07-22T22:17:46Z 2015-05 2015-04-28 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. 2015-5 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 application/pdf http://hdl.handle.net/2142/78502 en Copyright 2015 Andrew Russel Cholewa 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) Maude-PSL: a new input language for Maude-NPA text text Computer Science Computer Science University of Illinois at Urbana-Champaign Thesis M.S.