PaperlayerView exact revision on arXiv

Source-linked AI summary

Automatic Verification of Correspondences for Security Protocols

Bruno Blanchet

arXiv:0802.3444v1cs.CRcs.LO

TL;DR

The paper addresses automatic verification of correspondence properties for security protocols with unbounded sessions. It extends secrecy verification by translating annotated process-calculus protocols into Horn clauses and solving the resulting queries. The implemented technique verifies literature protocols efficiently, with reported experiments completing in less than 1 s.

  • Problem

    Security protocols need correspondence and authentication verification with an unbounded number of sessions, but general automatic verification cannot cover all protocols.

  • Method

    The protocol is represented in an extended pi calculus with cryptographic primitives and events, automatically translated into Horn clauses, and analyzed by a resolution-based solver.

  • Results

    The technique is fully automatic, supports unbounded sessions and general cryptographic primitives, and was implemented and tested on protocols from the literature.

  • Takeaways & Limitations

    The technique enables efficient automatic checking of correspondences, including authentication and expected message ordering, without bounding protocol sessions.

  • Takeaways & Limitations

    The abstraction is not complete: it may fail to prove some correct protocols, and the solving algorithm rarely fails to terminate.

Abstract

from arXiv · show

We present a new technique for verifying correspondences in security protocols. In particular, correspondences can be used to formalize authentication. Our technique is fully automatic, it can handle an unbounded number of sessions of the protocol, and it is efficient in practice. It significantly extends a previous technique for the verification of secrecy. The protocol is represented in an extension of the pi calculus with fairly arbitrary cryptographic primitives. This protocol representation includes the specification of the correspondence to be verified, but no other annotation. This representation is then translated into an abstract representation by Horn clauses, which is used to prove the desired correspondence. Our technique has been proved correct and implemented. We have tested it on various protocols from the literature. The experimental results show that these protocols can be verified by our technique in less than 1 s.

1 Introduction

The paper targets fully automatic verification of correspondences for security protocols with unbounded sessions. It extends secrecy analysis using Horn clauses and supports broad cryptographic models with limited user annotation.

  • Motivation: Unbounded-session protocol verification is difficult because insecurity is undecidable in general, while protocol errors emerge only against malicious adversaries.The paper situates its approach in the Dolev–Yao model and language-based verification techniques.
  • Contribution: The paper introduces fully automatic correspondence verification without bounding protocol sessions, including non-injective and injective correspondences.Correspondences express required prior events and can formalize authentication.
  • Method: The protocol is encoded in an extended pi calculus with cryptographic primitives and events, then translated automatically into Horn clauses for resolution-based verification.Events are the only required protocol annotation; no proof-oriented annotation is needed.
  • Capabilities and limits: The method is fully automatic, session-unbounded, and supports shared-key, public-key, signatures, hashes, and Diffie-Hellman key agreements.The solver may fail to terminate rarely, and the abstraction can fail to prove some correct protocols.
  • Implementation and prior work: The technique is implemented in ProVerif and has been extended from secrecy verification to correspondence properties.The paper also reports a process-level characterization of tagged protocols supporting termination results.

2 The Process Calculus

The paper models protocols as processes in an extended pi calculus with constructors, destructors, communication, restrictions, replication, conditionals, and events. Its example uses public-key Needham–Schroeder processes with unbounded sessions.

  • Terms and operations: The calculus represents terms as variables, names, and constructor applications, while destructors manipulate terms through partial rewrite-rule-defined functions.Destructor evaluation selects a successful branch or executes an else branch when no rewrite rule applies.
  • Process syntax: Processes include input, output, parallel composition, replication, name restriction, destructor application, conditionals, and event execution.The syntax is based largely on the pi calculus and adds event constructs for correspondence specifications.
  • Cryptographic primitives: The model supports cryptographic operations including tuple projection, shared-key and public-key encryption, signatures, hashes, and private key-table lookups.Constructors and destructors may be public or private, allowing adversary operations and honest-server tables to be modeled.
  • Operational semantics: Operational semantics reduces configurations containing environments and multisets of closed processes through rules for replication, parallelism, restriction, communication, destructors, and events.A semantic configuration is a pair consisting of a finite name environment and finite multiset of closed processes.
  • Example protocol: The running Needham–Schroeder example uses public channel c, public keys, nonces, and replicated principals that can execute an unbounded number of sessions.The protocol exchanges three public-key-encrypted messages and uses events to express authentication on shared nonce values.

3 Definition of Correspondences

Correspondences specify which prior events, messages, or attacker-knowledge facts must accompany a trace event. The framework supports logical combinations, parameter agreement, and injective or non-injective authentication properties.

  • General correspondences: A correspondence requires that when a trace satisfies one atom, a corresponding disjunctive set of events with matching arguments has already been executed.Variables in the triggering atom are universally quantified, while additional variables in consequent events are existentially quantified.
  • Trace semantics: The framework defines trace satisfaction for attacker knowledge, channel messages, and executed events under Dolev–Yao adversaries.An Init-adversary has free names only from the initial public-name set and contains no events.
  • Special cases: Secrecy is expressed as attacker(M) ⇝ false, while correspondence examples relate protocol completion events to role participation and agreement on nonce values.The same event-based framework therefore covers secrecy and authentication-style properties.
  • Non-injective correspondences: Non-injective agreement requires each event e(x1, ..., xn) to correspond to an event e′(x1, ..., xn) with the same parameters.This captures Lowe’s notion of non-injective agreement and can express authentication between protocol roles.
  • Injective correspondences: Injective correspondences require distinct matching prior events, whereas non-injective correspondences allow multiple triggering events to share one matching event.The injective marker applies to event correspondences in the stated formalism.

4 Automatic Verification: from Secrecy to Correspondences

The verification extends secrecy analysis by overapproximating protocol executions with Horn clauses while treating required correspondence events specially. Session identifiers preserve nonce distinctions needed for correspondence proofs.

  • Horn-clause representation: The analysis represents attacker capabilities and channel messages with Horn-clause predicates that encode computation, listening, sending, and protocol outputs.Derivable attacker(M) facts mean the adversary may possess M.
  • Event analysis: Correspondence verification adds event predicates to the secrecy analysis, overapproximating executions of triggering events while avoiding overapproximation of required events.Overapproximating required events could incorrectly suggest that a correspondence holds when those events are not actually executed.
  • Correspondence checking: The method fixes an exact allowed set E of required events and checks that only triggering events compatible with E are derivable for every value of E.The m-event predicate records membership in E and remains unevaluated during resolution.
  • Precision: Session identifiers distinguish names created in different replication copies, preventing nonce merging that could invalidate parameter agreement in correspondences.The earlier encoding could merge names created by the same restriction after identical inputs.

5 From Processes to Horn Clauses

The protocol is instrumented with session identifiers and structured name patterns, then translated into Horn clauses whose derivations preserve protocol traces and events. This abstraction supports sound correspondence proofs but may introduce false attacks because of implicit replication.

  • Instrumented Processes: Names are encoded as function patterns indexed by session identifiers and contextual values, preventing distinct generated names from being merged by the verifier.Each copy of a restriction receives different session-identifier values, so at most one name corresponds to a given encoded pattern in a trace.
  • Instrumented Processes: The instrumented semantics uses configurations containing unused session identifiers, an environment mapping names to patterns, and a finite multiset of processes.Replication consumes an unused session identifier to create a process copy, while restriction creates a fresh name.
  • Instrumented Processes: Replication and restrictions are instrumented with session identifiers and labels, producing an abstract process that represents unboundedly many protocol sessions.Replication variables identify process copies, while restriction labels record enclosing sessions and relevant inputs or destructor results.
  • Correctness: The abstraction preserves executions, events, and satisfied atoms between standard and instrumented traces, and correspondences proved for instrumented processes imply correspondences for standard processes.These results provide the semantic basis for transferring verification results back to the original protocol.
  • Approximation and Soundness: Horn-clause approximations can prevent proofs of some valid properties and produce false attacks, although proved security properties remain sound.Implicit replication over-approximates process behavior, while session identifiers prevent unrestricted repetition of name creation.

6 Solving Algorithm

The solving algorithm first saturates Horn clauses while preserving derivability, then uses backward depth-first search to determine whether a fact follows. Its correctness supports proving correspondences, including event-ordering properties.

  • Resolution and selection: Resolution combines clauses when a conclusion unifies with a selected hypothesis, using a most general unifier to construct the resulting clause.Free selection limits resolution to selected facts, reducing possible unifications while retaining completeness.
  • Resolution and selection: The selection function chooses at most one selectable fact per clause and never selects attacker(x) or m-event(p) hypotheses.This limits resolution choices and can substantially affect algorithm speed.
  • Overall structure: The algorithm has two phases: saturate simplifies clauses, while derivable uses backward depth-first search to test fact derivability.The phases are summarized in Figure 4.
  • First phase: saturation: Saturation repeatedly resolves clauses under a selection function, simplifies results, removes subsumed clauses, and returns clauses with no selected hypotheses.The three saturation steps initialize clauses, iterate resolution to a fixpoint, and return clauses whose selection is empty.
  • Correctness: Saturation preserves derivability under the stated secrecy condition, and the correctness lemmas characterize when derivable clauses establish a queried fact.The main correctness theorem uses these results to show that specified events must have been executed.
  • Second phase: derivability: The derivability phase performs a backward depth-first search, repeatedly resolving selected hypotheses until reaching a subsumption cycle or a clause with empty selection.The search starts from F ⇒ F and transforms its hypotheses using clauses from the saturated set.

7 Application to Correspondences

The paper develops automatic Horn-clause methods for proving non-injective, injective, and recent correspondences, including authentication-related properties, without bounding protocol sessions. The method is illustrated with formal theorems, examples, and conditions under which injectivity and recentness follow.

  • 7.1 Non-injective Correspondences: The verification method checks correspondences for instrumented processes by analyzing Horn clauses generated from the protocol.The proof connects clauses in solveP′0,Init(F) to events executed in protocol traces.
  • 7.1 Non-injective Correspondences: Theorem 4 establishes correspondences when every relevant derived clause contains hypotheses corresponding to the required preceding events.The trace proof instantiates the clause hypotheses and shows that the antecedent events were executed.
  • 7.2 General Correspondences: In the running example, the tool proves several correspondences, including recent injective agreement between eB and e3 and between eA and e2.It also derives a nested recent correspondence involving eB, e3, e2, and e1, while a direct nested proof can fail because replay may create multiple e2 events after one e1 event.
  • 7.1 Non-injective Correspondences: The framework also recovers secrecy and non-injective agreement as particular cases of correspondences.Secrecy is represented using attacker(M) ⇝ false, while non-injective agreement follows from event-implication conditions.
  • 7.2 General Correspondences: General correspondence results extend the analysis to injective correspondences and define recentness through overlap between the runtimes of corresponding sessions.Injective correspondence additionally prevents distinct executions from matching the same corresponding event.
  • 7.2 General Correspondences: The instrumented process records session identifiers on events, enabling recent injective agreement results under syntactic non-unification conditions.Corollary 3 states recent injective agreement when differently indexed event instances cannot unify.

8 Termination

The paper characterizes tagged protocols at the process level and proves termination of the solving algorithm for a specified class of correspondence queries. Tagged protocols use distinguishable constructor applications, enabling clause-level termination arguments.

  • 8.1 Termination for Tagged Protocols: Tagged protocols are processes whose constructor applications are distinguishable, typically by distinct constant tags checked by destructors.For example, encrypting m under k uses sencrypt((ct0, m), k), with a different tag for each encryption occurrence.
  • 8.1 Termination for Tagged Protocols: The process-level definition extends earlier clause-level termination results for tagged protocols.The clause-generation algorithm yields clauses satisfying the conditions previously known to guarantee termination.
  • 8.1 Termination for Tagged Protocols: For sel = sel0, the algorithm terminates on tagged protocols for queries α ⇝false when α and all facts in Fnot are closed.This is the stated termination proposition for the analyzed query class.
  • 8.1 Termination for Tagged Protocols: The termination proof relies on tagged clause patterns, trace-grounded instances, and at most one trace instance for each non-variable, non-data tagged pattern.These properties follow from the tagging conditions, the intended execution trace, and restrictions on pk and host arguments.
  • 8.1 Termination for Tagged Protocols: The technique can fail to terminate in rare cases, although the paper reports no such cases in experiments with real protocols.A deliberately constructed example exhibits non-termination, while the termination result covers tagged protocols satisfying the stated conditions.

9 Extensions

The framework is extended to equational theories, more precise destructor-failure handling, and staged protocols. These extensions support modeling primitives such as Diffie-Hellman key agreement and properties involving key compromise.

  • 9 Extensions: The verifier can handle some equational theories by relating traces in the equational model to traces using additional rewrite rules.A correspondence proved in the rewrite-rule model therefore implies the same correspondence in the equational-theory model.
  • 9 Extensions: The experiments use an equational theory for Diffie-Hellman key agreement, abstractly represented by functions f and f′ satisfying equation (23).The equation captures the parties’ ability to compute the same shared secret from exchanged public values.
  • 9 Extensions: Equational-theory support preserves syntactic-unification efficiency but cannot handle associative functions such as XOR with the described rewrite-rule treatment.The limitation arises because associative functions would generate infinitely many destructor rewrite rules.
  • 9 Extensions: The implementation models failed equality tests and destructor applications using the nounif predicate and dedicated solver simplification steps.nounif holds when no closed substitution makes the compared patterns equal, allowing failure branches to be represented more precisely.
  • 9 Extensions: Stages model a global clock and allow the verifier to express properties concerning key compromise, including forward secrecy scenarios.For session secrecy, the verifier queries an attacker fact for sessions not marked as compromised; underivability establishes the stated secrecy condition.

10 Experimental Results

Experiments on literature protocols show that ProVerif can analyze secrecy and authentication specifications, identify attacks, and prove satisfied properties. Termination depends on protocol structure and solver choices, while tagged protocols and selected encodings improve termination.

  • Experimental setup: The verifier was implemented in OCaml and tested on secrecy and authentication properties across literature protocols.The reported tests include fully modeled interactions with servers for several Needham-Schroeder, Woo-Lam, Denning-Sacco, Otway-Rees, and Yahalom variants.
  • Experimental setup: The analysis measures Horn-clause counts, resolution steps, total execution time, and results for several secrecy and agreement specifications.Execution times were measured on a Pentium M 1.8 GHz, with the reported time covering all specifications checked for each protocol.
  • Limitations: Successful proofs are sound, but nontermination and approximation-induced false attacks limit completeness and trace reconstruction for some cases.Trace reconstruction succeeds in the Figure 6 tests for secrecy and non-injective correspondences without key compromise, but is not implemented for key compromise or injective correspondences.
  • Termination: The tool terminates on many untagged protocols, while explicit or implicit message distinctions help explain termination in several examples.It terminates on all other Figure 6 protocols beyond those with explicit tags, and many terminating examples are not even implicitly tagged.
  • Authentication results: For Yahalom, the verifier establishes one directional agreement about the session key, whereas the converse fails because the adversary can intercept the final message.The resulting attack leaves A with the key while B does not have it.

11 Conclusion

The paper extends logic-programming verification from secrecy to general correspondences, including authentication and message-order properties. The resulting technique is fully automatic, handles unbounded sessions, and is efficient in experiments.

  • The technique extends previous secrecy verification to a broad class of correspondences, including authentication and expected message ordering.
  • It checks correspondences fully automatically without bounding the number of protocol sessions.
  • The resulting verifier is efficient, as demonstrated by the experimental results.

A Instrumented Processes

The instrumented-process semantics tracks session identifiers, environments, and closed processes while preserving labeling properties through reductions. Several lemmas establish how environments, substitutions, and traces relate between instrumented and ordinary executions.

  • Labels record restrictions, environments, and session identifiers, and well-labeled configurations contain no duplicate labels.
  • An instrumented semantic configuration consists of session identifiers, an environment mapping names to closed patterns, and a multiset of closed processes.
  • Reduction preserves well-labeling by moving or removing labels without introducing duplicates.
  • Environment mappings commute with substitutions for terms and atoms, with the result proved by structural induction.
  • Instrumented and ordinary traces satisfy corresponding atoms, enabling correspondence reasoning to transfer between the two semantics.

B Proof of Theorem 1

The correctness proof uses a type system to express process invariants and shows that well-typedness is preserved throughout executions. It connects executed events, messages, and attacker facts to derivable Horn-clause facts.

  • The type system expresses process invariants and adapts the earlier secrecy-verification type system to correspondences.
  • Types distinguish session identifiers, ordinary patterns, and environments, while type rules define the judgment E ⊢P.
  • A configuration is well-typed when it is well-labeled and every process in its multiset satisfies the typing judgment.
  • Subject reduction preserves well-typedness across reductions when executed events satisfy the required event facts.
  • Events, messages, and attacker observations in traces correspond to facts derivable from the generated Horn clauses.

C Correctness of the Solving Algorithm

The solving algorithm relies on resolution with free selection and clause simplifications, whose completeness is extended to the protocol setting. Data decomposition and node merging transform derivations while preserving their conclusions and reducing their size.

  • Soundness means that a protocol proved secure by the analysis actually satisfies the specified property, whereas completeness would require proving every secure protocol.
  • The basic binary-resolution algorithm with free selection remains complete after protocol-specific clause simplifications.
  • Well-sorted clauses ensure that non-session-identifier variables in conclusions also occur in non-m-event hypotheses, and resolution preserves this property.
  • A data-decomposed derivation applies data-destructor clauses to intermediate constructor facts before using them to prove other facts.
  • Resolution can merge two derivation nodes into one while preserving the derived fact and, under the stated selection condition, data decomposition.
  • Transforming derivations into data-decomposed form terminates because each replacement strictly decreases the total number of nodes.

D Termination Proof

The termination proof establishes that saturation and derivability terminate for weakly tagged programs, then applies these results to tagged protocols under stated conditions.

  • For tagged protocols with at most one element in Paramspk and Paramshost, condense(RP′0,Init) is a weakly tagged program.
  • The detailed proof is omitted and replaced by an approximately eight-page proof sketch.
  • Proposition 5 states that saturation terminates when condense(R0) is a weakly tagged program.
  • Generated clauses terminate because an instantiated clause size is bounded by the maximum initial protocol-clause size, yielding finitely many clauses.
  • Proposition 6 states that derivable(F, R1) terminates for simplified weakly tagged programs when sel0(R) = ∅ for every clause.
  • The proof ultimately concludes that the optimized algorithm terminates on P0 after establishing termination for the less optimized algorithm.

E General Correspondences

The paper extends correspondence verification to general event arguments by relating instrumented traces to matching earlier events and proving the required correspondence.

  • The trace argument shows that events of the relevant form have no duplicate session identifiers.
  • Lemma 18 constructs an injective function mapping each later m-event to an earlier matching event in the same trace.
  • The mapped earlier event occurs strictly before the later m-event, establishing the required temporal ordering.
  • The proof tracks three event sets across reductions and shows that the set of later m-events is included in the set of earlier events.
  • The transformed process P1 satisfies the correspondence, and the original process P0 inherits it through the generated clauses and verification procedure.
  • For each executed event, the construction recursively identifies corresponding events and substitutions satisfying the correspondence conditions.
Loading 0802.3444v1…