A Symbolic Logic with Concrete Bounds for Cryptographic Protocols
This work addresses the need for precise security guarantees in network protocols, though it appears incremental as it builds on existing formal methods and cryptographic primitives.
The authors tackled the problem of deriving concrete security bounds for cryptographic protocols by introducing a formal logic that supports quantitative reasoning, enabling the selection of key lengths and security parameters with proven authentication properties for a signature-based challenge-response protocol.
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.