Protocol trust requirements precisely identified for better security decisions
Trust a Few: The Weakest Assumptions a Protocol Needs
Cryptography and Security
Summary
Security protocols rely on trusting certain things to keep data safe, like secret keys or secure channels. The paper finds the minimal set of trust assumptions needed to guarantee a protocol’s security goal, avoiding unnecessary or excessive trust. The authors provide a method to calculate these weakest trust sets and prove some complexity limits. They test their approach on common protocols, showing it can identify subtle needed assumptions.
What this means in practice
- •For security protocol developers: Determine exactly which trust assumptions are essential to meet a protocol’s security goals, improving design and verification precision.
- •For network security engineers: Identify minimal channel and key trust requirements to better configure and deploy secure communication systems.
Authors
Bhumika Mittal, Aalok Thakkar
Abstract
Protocol verifiers check whether a protocol meets a security goal under stated trust assumptions, such as that a key is never leaked, a value is fresh, or a channel is authentic. They do not say which of those assumptions the goal needs. Rowe, Guttman and Liskov asked for the weakest assumptions under which a protocol achieves a goal and left the question open. We answer it for assumptions about keys, values and channels. Call a run that violates the goal an attack, and the assumptions that would rule it out its stopping set. The least a protocol must trust to meet a goal is exactly the set of minimal ways to stop all of its minimal attacks. Several such sets may exist. The answer becomes unique once either/or assumptions are allowed, and it is a single set exactly when every minimal attack is stopped by a single assumption. A Galois connection between assumptions and goals explains why: a goal may end in "or", but its hypothesis may not. The same structure gives the trust needed by a conjunction of goals and an exact condition under which composed protocols need no extra trust. To compute the answer, a loop asks a verifier whether a candidate suffices, records what stops each attack it reports, and recomputes the candidates. Deciding whether some trust of at most k assumptions suffices is NP-hard. With a bounded analyser of our own and with CPSA, the loop finds the weakest trust for 18 goals over ten protocols and their variants, and on each it agrees with evaluating every trust using the same verifier. The answers include an assumption that our model of the adopted fix of Kerberos PKINIT states but the client's authentication of the server does not need, and channel assumptions under which Needham-Schroeder meets its goal in a bounded model.