Files in this item



application/pdfYANG-DISSERTATION-2019.pdf (930kB)Restricted Access
(no description provided)PDF


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
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
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)

Item Statistics