Extending the language and applications of Maude-NPA through rewriting semantics

Yang, Fan

Permalink

https://hdl.handle.net/2142/105198 Copy

Description

Title

Extending the language and applications of Maude-NPA through rewriting semantics

Author(s)

Yang, Fan

Issue Date

2019-04-16

Director of Research (if dissertation) or Advisor (if thesis)

Meseguer, José

Doctoral Committee Chair(s)

Meseguer, José

Committee Member(s)

• Agha, Gul
• Roşu, Grigore
• Meadows, Catherine
• Escobar, Santiago

Department of Study

Computer Science

Discipline

Computer Science

Degree Granting Institution

University of Illinois at Urbana-Champaign

Degree Name

Ph.D.

Degree Level

Dissertation

Keyword(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.

Graduation Semester

2019-05

Type of Resource

text

Permalink

http://hdl.handle.net/2142/105198

Copyright and License Information

Copyright 2019 Fan Yang

Owning Collections