Finitary Deduction Systems

TL;DR

This paper introduces finitary deduction systems to unify the analysis of cryptographic protocol security, showing that equivalence properties for on-line attackers can be reduced to reachability problems within these systems.

Contribution

It proposes a new class of deduction systems that connect trace-based and equivalence-based security analyses, enabling reductions between different attack models.

Findings

Deciding equivalence properties reduces to reachability in finitary deduction systems.

Finitary deduction systems unify analysis approaches for on-line and offline attackers.

The approach simplifies security verification processes in cryptographic protocols.

Abstract

Cryptographic protocols are the cornerstone of security in distributed systems. The formal analysis of their properties is accordingly one of the focus points of the security community, and is usually split among two groups. In the first group, one focuses on trace-based security properties such as confidentiality and authentication, and provides decision procedures for the existence of attacks for an on-line attackers. In the second group, one focuses on equivalence properties such as privacy and guessing attacks, and provides decision procedures for the existence of attacks for an offline attacker. In all cases the attacker is modeled by a deduction system in which his possible actions are expressed. We present in this paper a notion of finitary deduction systems that aims at relating both approaches. We prove that for such deduction systems, deciding equivalence properties for on-line attackers can be reduced to deciding reachability properties in the same setting.