2026-09-19T14:38:16Z https://www.ideals.illinois.edu/oai-pmh

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

Meseguer, José Meseguer, José Agha, Gul Roşu, Grigore Meadows, Catherine Escobar, Santiago Yang, Fan 2019-08-23T20:47:24Z 2019-08-23T20:47:24Z 2021-08-24T09:15:10Z 2019-04-16 2019-05 Formal methods have been used in analyzing cryptographic protocols since the 1980’s. Formal analysis of cryptographic protocols involves properties that are generally undecidable; however it can often be automated. Maude-NPA is a special-purpose tool for verifying cryptographic protocols. Based on rewriting logic, Maude-NPA performs backward symbolic model checking on the unbounded session model, considering user defined signature and a wide range of equational theories. In this way, various properties, including secrecy, authentication and indistinguishability can be verified. This thesis investigates and advances cryptographic protocol modeling and analysis, with a focus on extending the specification and analysis capabilities of the Maude-NPA tool. In particular, (i) it presents a hierarchy of FVP theories for approximating the algebraic property of homomorphic encryption over an Abelian group, which enables analysis of protocols having homomorphic encryption over abelian group in Maude-NPA; (ii) it extends the strand space model with support for choice, and develops a protocol process algebra with choice constructors; as a result, a new specification language is provided for Maude-NPA, and protocols with choices can be model and analyzed naturally in Maude-NPA; (iii) it develops a methodology for modular analysis of protocol composition for private channels: the security properties of the composed protocols are decomposed into corresponding properties of each component protocols. In each of these areas (i)-(iii), experiments are performed in Maude-NPA to illustrate and validate these approaches. Submission published under a 24 month embargo labeled 'Closed Access', the embargo will last until 2021-05-01 The student, Fan Yang, accepted the attached license on 2019-04-15 at 14:54. The student, Fan Yang, submitted this Dissertation for approval on 2019-04-15 at 15:25. This Dissertation was approved for publication on 2019-04-16 at 13:59. DSpace SAF Submission Ingestion Package generated from Vireo submission #13634 on 2019-08-22 at 16:21:28 Made available in DSpace on 2019-08-23T20:47:24Z (GMT). No. of bitstreams: 2 YANG-DISSERTATION-2019.pdf: 930427 bytes, checksum: 1a8932d53a0d9238c7a254ff3ac022b2 (MD5) LICENSE.txt: 4205 bytes, checksum: 0aacd142e7fa251f8921c302fc08daf4 (MD5) Previous issue date: 2019-04-16 Embargo set by: Seth Robbins for item 112319 Lift date: 2021-08-23T20:47:38Z Reason: Author requested closed access (OA after 2yrs) in Vireo ETD system Embargo set by: Seth Robbins for item 112319 Lift date: 2021-08-23T20:48:32Z Reason: Author requested closed access (OA after 2yrs) in Vireo ETD system Limited Restriction Lifted for Item 112319 on 2021-08-24T09:15:10Z. application/pdf http://hdl.handle.net/2142/105198 en Copyright 2019 Fan Yang formal analysis of cryptographic protocols rewriting logic process algebra Extending the language and applications of Maude-NPA through rewriting semantics text text Computer Science Computer Science University of Illinois at Urbana-Champaign Dissertation Ph.D.