Files in this item
Files | Description | Format |
---|---|---|
application/pdf ![]() ![]() | (no description provided) |
Description
Title: | Extending the language and applications of Maude-NPA through rewriting semantics |
Author(s): | Yang, Fan |
Director of Research: | Meseguer, José |
Doctoral Committee Chair(s): | Meseguer, José |
Doctoral Committee Member(s): | Agha, Gul; Roşu, Grigore; Meadows, Catherine; Escobar, Santiago |
Department / Program: | Computer Science |
Discipline: | Computer Science |
Degree Granting Institution: | University of Illinois at Urbana-Champaign |
Degree: | Ph.D. |
Genre: | Dissertation |
Subject(s): | formal analysis of cryptographic protocols
rewriting logic process algebra |
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. |
Issue Date: | 2019-04-16 |
Type: | Text |
URI: | http://hdl.handle.net/2142/105198 |
Rights Information: | Copyright 2019 Fan Yang |
Date Available in IDEALS: | 2019-08-23 |
Date Deposited: | 2019-05 |
This item appears in the following Collection(s)
-
Dissertations and Theses - Computer Science
Dissertations and Theses from the Dept. of Computer Science -
Graduate Dissertations and Theses at Illinois
Graduate Theses and Dissertations at Illinois