Secure Process Algebra

TL;DR

This paper introduces Secure APTC, a formal algebraic framework based on truly concurrent process algebras, for verifying security protocols with rich expressive power and strong theoretical foundations.

Contribution

It develops Secure APTC with equational logics, operational semantics, and axiomatizations, enabling comprehensive modeling and analysis of security protocols including cryptographic operations and attacks.

Findings

Secure APTC can model cryptographic operations as atomic actions.

It provides a clear framework to analyze protocol relations under various attack scenarios.

The algebraic approach facilitates verification of security properties in protocols.

Abstract

Based on our previous work on truly concurrent process algebras APTC, we use it to verify the security protocols. This work (called Secure APTC, abbreviated SAPTC) have the following advantages in verifying security protocols: (1) It has a firmly theoretic foundations, including equational logics, structured operational semantics, and axiomatizations between them; (2) It has rich expressive powers to describe security protocols. Cryptographic operations are modeled as atomic actions and can be extended, explicit parallelism and communication mechanism to modeling communication operations and principals, rich computational properties to describing computational logics in the security protocols, including conditional guards, alternative composition, sequential composition, parallelism and communication, encapsulation and deadlock, recursion, abstraction. (3) Especially by abstraction, it is convenient and obvious to observe the relations between the inputs and outputs of a security protocols, including the relations without any attack, the relations under each known attack, and the relations under unknown attacks if the unknown attacks can be described.