{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/105198"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/105198","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Extending the language and applications of Maude-NPA through rewriting semantics","abstract":"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.","abstract_html":"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.","abstract_has_math":false,"creators":["Yang, Fan"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"Ph.D.","degree_level":"Dissertation","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":["Meseguer, José","Agha, Gul","Roşu, Grigore","Meadows, Catherine","Escobar, Santiago"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2019,"date_issued":"2019-08-23T20:47:24Z","date_published":"2019-08-23T20:47:24Z","updated_at":"2026-07-22T22:24:44Z","subjects":["formal analysis of cryptographic protocols","rewriting logic","process algebra"],"languages":["en"],"rights":["Copyright 2019 Fan Yang"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/2142/105198","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Meseguer, José","Agha, Gul","Roşu, Grigore","Meadows, Catherine","Escobar, Santiago"]},{"key":"dc:creator","label":"Author","values":["Yang, Fan"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2019-08-23T20:47:24Z","2021-08-24T09:15:10Z","2019-04-16","2019-05"]},{"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":["Dissertation"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Ph.D."]},{"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":["formal analysis of cryptographic protocols","rewriting logic","process algebra"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2019 Fan Yang"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/105198"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["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."]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Extending the language and applications of Maude-NPA through rewriting semantics"]}]}],"canonical_facts":{"dc:contributor":["Meseguer, José","Agha, Gul","Roşu, Grigore","Meadows, Catherine","Escobar, Santiago"],"dc:creator":["Yang, Fan"],"dc:date":["2019-08-23T20:47:24Z","2021-08-24T09:15:10Z","2019-04-16","2019-05"],"dc:description":["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."],"dc:format":["application/pdf"],"dc:identifier":["http://hdl.handle.net/2142/105198"],"dc:language":["en"],"dc:rights":["Copyright 2019 Fan Yang"],"dc:subject":["formal analysis of cryptographic protocols","rewriting logic","process algebra"],"dc:title":["Extending the language and applications of Maude-NPA through rewriting semantics"],"dc:type":["text"],"thesis:degree_discipline":["Computer Science"],"thesis:degree_level":["Dissertation"],"thesis:degree_name":["Ph.D."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:24:44Z"}