A Symbolic Logic with Concrete Bounds for Cryptographic Protocols

TL;DR

This paper introduces a formal logic framework for analyzing cryptographic protocols that provides concrete security bounds, enabling precise parameter selection and combining asymptotic and concrete security guarantees.

Contribution

It presents a novel formal logic system for quantitative security reasoning that incorporates concrete bounds for cryptographic primitives and protocol invariants.

Findings

Derived concrete security bounds for digital signatures and PRGs.

Proved an authentication property with explicit bounds in a challenge-response protocol.

Integrated concrete and asymptotic security guarantees in protocol proofs.

Abstract

We present a formal logic for quantitative reasoning about security properties of network protocols. The system allows us to derive concrete security bounds that can be used to choose key lengths and other security parameters. We provide axioms for reasoning about digital signatures and random nonces, with security properties based on the concrete security of signature schemes and pseudorandom number generators (PRG). The formal logic supports first-order reasoning and reasoning about protocol invariants, taking concrete security bounds into account. Proofs constructed in our logic also provide conventional asymptotic security guarantees because of the way that concrete bounds accumulate in proofs. As an illustrative example, we use the formal logic to prove an authentication property with concrete bounds of a signature-based challenge-response protocol.