+ +

Computational Soundness for Formal

Adversaries

Jonathan Herzog CIS, TOC, LCS, MIT

(Joint work w/ Ron Rivest, Nancy Lynch)

+ +

Needham–Schroeder Public Key Protocol

First published public-key protocol (1978)

1. A ⟶ B: {|N_{a} A|}_{K_{B}}

2. B ⟶ A: {|N_{a} N_{b}|}_{K_{A}}

3. A ⟶ B: {|N_{b}|}_{K_{B}}

A, B are principals

– K_{A}: public key of A {|M|}_{K} is the encryption of M in key K N_{a}, N_{b} are fresh random values (“nonces”) Designed to provide mutual authentication and secrecy of N_{a}, N_{b}

+ +

How to Analyze?

Cryptographic protocols can be analyzed using the same tools used for primitives (Bellare & Rogaway 1994, 1995) However, “computational” model not the only framework for protocol analysis Dolev-Yao (“formal”) model developed in formal methods community

– Reflects character of that field Both have advantages; how do they relate? This talk:

– Explain formal model

– Examine relationship between computational and formal models in one key area: the adversary

+ +

Overview

Motivation A security definition Implementation and proof

+ +

NS Protocol: Initiator’s view

Initiator’s authentication goal: If A sees view on left, then B sees view on right

A \overline{\{|N_{a} A|\}_{K_{B}} ▶}  \overline{\{|N_{a} A|\}_{K_{B}} ▶} B
•^{‖}◀ \{|N_{a} N_{b}|\}_{K_{A}}  ◀ \underline{\{|N_{a} N_{b}|\}_{K_{A}}} •^{‖}
•^{‖}  \overline{\{|N_{b}|\}_{K_{B}} ▶}  \overline{\{|N_{b}|\}_{K_{B}} ▶} •^{‖}

(except possibly last step) How to see this:

– Fresh nonce N_{a} sent out encrypted in B’s public key – Received back

– Someone must have decrypted it

– B must be out there, with corresponding view

+ +

NS Protocol: Responder’s View

Responder’s authentication goal: If B sees view on right, then A sees view on left

A \overline{\{|N_{a} A|\}_{K_{B}} ▶}  \overline{\{|N_{a} A|\}_{K_{B}} ▶} B
•^{‖}◀ \underline{\{|N_{a} N_{b}|\}_{K_{A}}}  ◀ \{|N_{a} N_{b}|\}_{K_{A}} •^{‖}
•^{‖}  \{|N_{b}|\}_{K_{B}} ▶  \overline{\{|N_{b}|\}_{K_{B}} ▶} •^{‖}

– How to see this: B sends out fresh random value N_{b} in A’s public key N_{b} comes back Someone must have decrypted it A must be out there, with corresponding view

+ +

Very Simple Adversary

Consider simple adversary: Presumed to start knowing some initial set of messages

– Can guess predictable values Intercepts every message sent by honest participant Can perform only the following operations:

– Encrypt known message with public key

– Decrypt known message with known private key

– Separate a known pair

– Pair two known messages

– Generate new nonces, keys Can perform finite number of such operations before sending known message to any honest participant

+ +

Demo 1

Such an adversary can be specified as simple state machine Honest participants also simple state machines Behavior individual state machines can be composed into larger machine Security goals expressable as properties A safety property: “bad things” never happen. A liveness property: “good things” eventually do happen. All security properties are safety properties of the larger system Many tools exist to check system against goals

– This example: Murϕ State exploration tool for finite systems. (Dill, et. al.) http://verify.stanford.edu/dill/murphi.html

+ +

Needham-Schroeder: Flawed!

A  \overline{\{|N_{a} A|\}_{K_{M}} ▶} M
•^{‖}  \overline{\{|N_{a} A|\}_{K_{B}} ▶} B
•^{‖}◀ \underline{\{|N_{a} N_{b}|\}_{K_{A}}}  ◀ \{|N_{a} N_{b}|\}_{K_{A}}  •^{‖}
•^{‖}  \overline{\{|N_{b}|\}_{K_{M}}  ▶} M
•^{‖}  \overline{\{|N_{b}|\}_{K_{B}}  ▶} •^{‖}

Due to Gavin Lowe ( 1995 \begin{matrix}Partial reason for delay: \\ Original analysis assumed everyone with public key to be trustworthy. \\ Assumption perhaps valid in 1978, not so valid in 1995 \end{matrix} ) – Found using automated tool FDR, much more powerful than Murϕ !

+ 2002.10.27  9

+ +

Dolev–Yao Model

Dolev-Yao model: Adversary is simple Pros:

– Very easy to work in

– Need only consider specific adversary

– Short proofs Re-usable general theorems

– Automation Find flaws automatically Develop proofs automatically Technically, the general problem is undecidable. Tools either risk non-termination or require work on part of user

– Good for examining structure of protocols Cons:

– Well...best explained by example

+ +

Needham–Schroeder–Lowe Protocol

Lowe “fixed” NS protocol by adding B’s name to second message:

A  \overline{\{|N_{a} A|\}_{K_{B}}  ▶} B
•^{‖}◀ {|B N_{a} N_{b}|}_{K_{A}}  •^{‖}
•^{‖}  \overline{\{|N_{b}|\}_{K_{B}}  ▶} •^{‖}

Murϕ finds no flaws (Demo 2)

– Murϕ doesn’t generate proofs, but...

– Can also be proven no flaw exists in Dolev-Yao model

– Hence, secure against formal adversary What can we conclude, really?

+ +

Tale of Two Models

Viewing the computational model as a “semantics” for the formal model: Formal model is complete

– Any flaw found in formal model will exist in computational

model Would like formal model to be sound

– Proof of correctness in formal model implies correctness in computational model

– Much less work for us Any demonstration of soundness will involve many components Here, we focus entirely on adversary

Point of this talk: show cryptography can limit computational adversary to formal adversary

+ +

Related Work

This work greatly inspired by Abadi and Rogaway (2000)

– Their work considered weaker Mapping indistinguishability from formal to computational model. Our work considers full formal adversary computational adversary Incorporating poly-time indistinguishability into process calculus (Mitchel et al. 1998,1999,2001)

+ +

Overview

Motivation A security definition Implementation and proof

+ +

Formal Adversary Revisited

Want to limit computational adversary to formal adversary One way to represent a formal adversary is by its possible attacks

– Sequence of (adversary) queries, (participant) responses

R_{0} Q_{1} R_{1} … Q_{n−1} R_{n−1} Q_{n} R_{n}

Each query Q_{i} must be derivable from initial adversary knowledge (S_{0}), all previous responses If S is a set of messages, C [S] is the smallest set so that

– S ⊆ C [S],

– S is closed under pairing, separation

– S is closed under encryption, decryption with keys in S Want that

Q_{i} ∈ C [S_{0} ∪ {R_{0}, R_{1}, … R_{i−1}}]

+ +

Generalizing Formal Adversary

Two reasons to generalize constraint slightly

1.Protocol independence – Don’t know what R_{0}, R_{1}… R_{i−1} will look like

– Wouldn’t want a protocol-specific result anyway 2.Initial knowledge

– Don’t know what will be in S_{0}

– Will contain public values, its own nonces, etc.

– Might contain arbitrary other things More general constraint on adversary:

If formal adversary “knows” messages in set S, can only make

messages in C [S]

Assumption: S contains all public values (names, public keys, etc.)

+ +

Ideal Encryption — Take 1

How do we enforce this constraint? Through cryptography! An encryption operation is ideal if

∀ A_{PPT} ,

∀ sets of messages S

∀ M ∉ C [S], ∀ c > 0, ∀ s.l. k, Pr[m ← A(S) : m = M] ≤ \frac{1}{k^{c}}

Wait a second here... This makes no sense!

+ +

Message Encoding

Must bring formal messages down into the world of bit-strings Let [[M]]_{k} be the encoding of M

– Function Technically, we define set of encoding functions, each mapping atomic messages to single values. Later, will pick random encoding function from M to distributions on bit-strings Defined recursively:

– [[N]]_{k} is a random k-bit string

– [[K]]_{k} generated by key generation algorithm (run on 1^{k})

– [[A]]_{k} can be defined any way you like

– [[M_{1} M_{2}]]_{k} is the (tagged) concatenation of [[M_{1}]]_{k} and [[M_{2}]]_{k} – [[{|M|}_{K}]]_{k} made from [[M]]_{k} and [[K]]_{k} using arbitrary public-

key encryption algorithm Can think of encryption algorithm as parameter of conversion operation

+ +

Ideal Encryption — Take 2

An encryption operation is ideal if, when used in [[·]]_{k}:

∀ A_{PPT} , ∀ sets of messages S, ∀ M ∉ C [S], ∀ c > 0, ∀ s.l. k,

Pr[ s Here, we choose encoding function randomly from all encoding functions ← [[S]]_{k}; m ← A(1^{k}, s) : m ∈ [[M]]_{k} supp([[M]]_{k}) ] ≤ \frac{1}{k^{c}}

If M is atomic, [[M]]_{k} has one element If M is compound, [[M]]_{k} may be non-trivial distribution

+ +

Adversary Reduction

Definition discusses a single query of the adversary

– If computational adversary creates valid encoding, then only

likely messages are in closure Adversary gets to make n queries! But n (# of queries) is constant with respect to k Union bound demonstrates closure respected over all n queries Thus: if computational adversary only creates valid encodings, must mimic formal adversary

Says nothing about garbage queries – Would require discussion of honest participants

– Subject of another (later) talk

+ +

Overview

Motivation A security definition Implementation and proof

+ +

Implementing Ideal Encryption

Ideal cryptography no good unless it can be achieved Thm: Let E_{e}(m) produce two things:

– c ← E′_{e}(m), where E′ is a (one-pass) One-pass: secures even messages related to public key Three-pass: secures only messages independent of public key GM-secure encryption scheme, and

– p ← P(c, ⟨m, r, e⟩ , O(c)), where P is the prover for a NIZK PK system, r is the randomness used to make c, and O(·) is the random oracle,

Then E is ideal.

+ +

Proof (1/4)

Look at parse tree of M. If all paths from root to leaf go through element in C [S], root is in closure. Why? If both children in C [S], then parent in C [S].

[figure: N_{1}; N_{2}; N_{1} N_{2}; K; {|N_{1} N_{2}|}_{K}; A; {|N_{1} N_{2}|}_{K} A]

+ +

Proof (2/4)

If all paths go through C [S], then root is in C [S]. Know this is not the case. Hence, at least one path does not go through C [S]

[figure: N_{1}; N_{2}; N_{1} N_{2}; K; {|N_{1} N_{2}|}_{K}; A; {|N_{1} N_{2}|}_{K} A]

+ +

Proof (3/4)

Along this path: If adversary can create parent, can create both children. Easy to undo pair operation. If adversary can create ciphertext, can create plaintext. (Thanks to NIZK PK in encryption.) Hence, adversary can create some leaf not in C [S].

[figure: N_{1}; N_{2}; N_{1} N_{2}; K; {|N_{1} N_{2}|}_{K}; A; {|N_{1} N_{2}|}_{K} A]

+ +

Proof (4/4)

Adversary can create encoding of some atomic element M′ not in C [S] M′ cannot be public information

– Must be nonce or private key Two cases Case 1: M′ is component of “in parse tree of”something in C [S]

– Example: {|N_{1}|}_{K} ∈ C [S] even though N_{1} ∉ C [S]

– Then M′ must be only plaintext of encryptions

– Hence, adversary able to break encryption scheme Case 2: M′ not component of something in C [S]

– Then adversary able to guess random nonce/key from independent values

+ +

Conclusions

Ideal encryption can be instantiated. This means… Possible to limit computational adversary to attacks available to formal adversary. This means… The Dolev-Yao model might have computational semantics, which would mean… Automatic verification of cryptographic protocols (to our satisfaction) might be possible

+ +

Open Questions

Other cryptographic operations

– Signatures, symmetric encryption, etc. How to deal with honest participants?

– Behavior in error cases usually unspecified

– Error codes might leak information How does definition of ideal cryptography relate to other definitions?

– Definition seems similar to “plaintext-aware” encryption

– Construction seems similar to constructions of schemes secure against CCA

+ +

Miscellany

Written in L^{A}TEX. Presented using ActiveDvi^{http://pauillac.inria.fr/advi/} , the “presentation tool of choice for the discriminating hacker” Housewarming party! Saturday night!

+ +

Proofs of Knowledge

Let L ∈ NP have witness relation W. Then (P, V, S = (S_{1}, S_{2}), E ) is a NIZK PK system for L if:

1.Everyone has access to common random (“reference”) string 2.Completeness: All true statements can be proved

– If x ∈ L, P has access to (x, w) ∈ W, P can send a p to

V such that V(x, w) accepts. 3.Soundness: hard to “prove” false statements

– If x ∉ L, adversary A generates p, chances of V(x, w)

accepting is small. 4.Simulatability: Adversary gains nothing from P

– Adversaries act the same whether they access (random string, P who has access to w ) or (S_{1}, S_{2} who does not have access to w )

– Hence, no adversary needs access to prover

– Mostly useful for proofs via reductions

+ +

Proofs of Knowledge

5.Extractability: If adversary can create fresh proof, then related adversary can produce witness

If A can, with probability P, produce a pair (x, p) so that V(x, p) accepts, then E (with access to A) can create w so that (x, w) ∈ W. For our talk:

– (x, p) is a ciphertext

– w is the plaintext Hence, if A can create “new” ciphertext, a related adversary E^{A} can create the plaintext