Transcript Computer-aided generation/verification of

A Plausible Approach
to Computer-aided
Cryptographic Proofs
Shai Halevi
June 2005
The Problem
• Crypto proofs are hard to verify
• Many (most?) published proofs aren’t
read by anyone other than the author
– Even proofs for “important” schemes are
often not fully verified
• Errors in proofs happen
– Usually in some itty-bitty detail in this
side remark at the bottom of page 27
June 2005
Sample Arguments
“We now make several changes to the
order in which variables are chosen in
game R1. We make the following changes
to the code:
– […]
– Instead of choosing MMs{0,1}n and setting
CsmPsmMMs, we choose Csm{0,1}n and
set MMsPsmCsm
– We replace the assignment CCCsiMCsjMs1 in
line 136 by the equivalent assignment
CCCsiPPPsiMsj. This is equivalent since
MCsj = MPsjMsj = PPPsiMs1Msj
– […]
June 2005
More Sample Arguments
“H6 checks in client sessions (Pi,ssid) that receive a non-peeroracle-generated pair […]
H7 encrypts the “dummy password” w’ in c2 instead of
encrypting the password w, for every client session (Pi,ssid)
that received a non-peer-oracle-generated pair (c1,VK) in
step 2 with non-valid ciphertext c1.
Then as in H2 and H4, since the encryption scheme E' is
semantically secure, the environment cannot distinguish
between these cases. Note that the session key of such
client sessions are already chosen randomly, and the ZKPs
are already simulated. Thus neither depends on how c2 is
generated. Also note that in the reduction to the security of
E' with public key pk', one can still test c1 encryptions, since
they are encrypted with the other public key pk and can be
decrypted using sk.”
June 2005
You need to be a compiler
to verify some of these
arguments
June 2005
Can We Write Such Compiler?
• Boils down to verifying that two
pieces of code induce the same
probability distribution on some of
their variables
• The simplest example:
M{0,1}n, CPM, Use(C) vs.
C{0,1}n, MPC, Use(C)
June 2005
In This Talk
• Look at the security-proof of the
Cramer-Shoup encryption scheme
• Show how to reconstruct the proof
using a “compiler-like” tool
• Muse about how to build this tool
June 2005
My Bottom Line
• It can be built, with a lot of work
– Perhaps similar to a new programming
language: compiler, run-time,
development environment, …
• Is there a “business case”?
– Where can I get resources to develop
this tool?
June 2005
This tool is not…
• Not a theorem prover
– A person writes the (entire) proof
– The tool only verifies that the
arguments are valid
• Different than the approach of the
formal-methods community (AFAIK)
– No “logic of authentication”, “process
calculus”, etc.
June 2005
Computer assistance
• The person writing the security proof
writes code, specifies how to get
from one piece of code to the other
• The automated tool verifies that the
transformations are permissible
– Transformations to code represent
common arguments in crypto proofs
June 2005
Preview: The Proof of CS98
DDH
+DDH
TCR
+TCR
+t /q^4
CCA4
CCA1
+1/q
XYZ
+epsilon
CCA1
CCA5
CCA2
CCA[CS]
CCA
CCA5’
CCA2
CCA3’
+2t / q
CCA4
CCA5
game with bad events
game with output
game that depends on a (binary) parameter
The empty game
game that is derived from template XYZ
transformation that changes the probability by epsilon
transformation that is justified by a reduction
June 2005
Everything is code
• Game = code that tells the
participants in the game what to do
• Argument in a proof =
transformation from one game to
another
June 2005
The Cramer-Shoup
Encryption Scheme
• Uses operations in algebraic group G
• And a hash function H
• Resists chosen ciphertext attacks,
provided that
– The “decision Diffie-Hellman” problem
(DDH) is hard in the group G
– The hash function H is “target-collisionresistant”
June 2005
Pseudo-code for CS98
KeyGen
01. g,g’G, x1,x2,y1,y2,z1,z2{1,2,…,q}
02. e=gx1g’x2, f=gy1g’y2, h=gz1g’z2
03. pk=(g,g’,e,f,h), sk=(x1,x2,y1,y2,z1,z2)
Enc(m)
11.
12.
13.
14.
15.
assert m  G
// else fail
u  {1,2,…,q}
a=gu, a’=g’u, b=hu, c=b·m
v=H(a,a’,c), d=eufuv
Output (a,a’,c,d)
Dec(a,a’,c,d)
21.
22.
23.
24.
25.
assert a,a’,c,d  G
// else fail
v = H(a,a’,c)
assert d = ax1+vy1·a’x2+vy2 // else fail
b = az1a’z2, m=c/b
Output m
June 2005
CCA Security
• “Resistance to chosen-ciphertext
attacks” is defined via a game
– Attacker gets public-key and access to
a black box that decrypts
– Attacker submits two messages, gets
back encryption of one of them, needs
to guess which one
• without asking the box to decrypt the
“target ciphertext”
June 2005
Pseudo-code for CCA Game
CCA (parameters: bit s, integer t)
101. (ps,sk)  KeyGen
102. C[1] = Attacker(pk)
103. For s=1 to t
104.
answer[s] = Dec(C[s])
105.
if s<t then C[s+1] = Attacker( answer[s] )
106. (m0,m1) = Attacker( answer[t] ), C* = Enc(ms)
107. C[t+1] = Attacker( C* )
108. For s=t+1 to 2t
109.
assert C[s]  C*
110.
answer[s] = Dec(C[s])
111.
if s<2t then C[s+1] = Attacker( answer[s] )
112. guess = Attacker( answer[2t] ), Output guess
June 2005
Proving Security
• Pasting CS98 in CCA, we get the code
describing CCA attack on CS98
• Fix any Attacker and any integer t
• Prove that CCA(0,t),CCA(1,t) output 1
with about the same probability
– We show:
|Pr[CCA(0,t)1] - Pr[CCA(1,t)1]|
 2DDH+Collisions+O(t/q)
June 2005
Some Concepts
• Games are specified via code
– With an unspecified “attacker function”,
– and a “main loop” where the attacker
queries interfaces of the scheme, gets
answers, then makes more queries…
• Most (all?) games are probabilistic
– E.g., u{1,2,…,q} in Enc(m)
• Every game has variables of interest
June 2005
Variables of Interest
• What “we care about” in the analysis
• These are always either:
– The output of the game
– Or bad events (I’ll talk about these later)
• Code that has no effect on the
variables-of-interest is dead code
– It is always permissible to add/remove
dead code
June 2005
Back to CCA Game
• The CCA game has output, no bad
events, and no dead code
– It is really two games, depending on the
value of the binary parameter s
– And we compare the output distribution
of the two games
• In games with output we always(?)
compare the output of two games
June 2005
The CS98 Proof
DDH
+DDH
TCR
+TCR
+t /q^4
CCA4
We are here
CCA1
+1/q
XYZ
+epsilon
CCA1
CCA5
CCA2
CCA[CS]
CCA0
CCA5’
CCA2
CCA3’
+2t / q
CCA4
CCA5
game with bad events
game with output
game that depends on a (binary) parameter
The empty game
game that is derived from template XYZ
transformation that changes the probability by epsilon
transformation that is justified by a reduction
June 2005
Game CCA1
• Modify the encryption code
Instead of
12. u  {1,2,…,q}
13. a=gu, a’=g’u, b=hu, c=b·m
14. v=H(a,a’,c), d=eufuv
We now have
12. u  {1,2,…,q}
13. a=gu, a’=g’u, b=az1a’z2, c=b·m
14. v=H(a,a’,c), d=ax1+vy1a’x2+vy2
• Encryption using the secret key?
– Yes, so? This is a “mental experiment”
• (BTW, the point about CCA1 is that
u is only used in computing a, a’)
June 2005
CCACCA1 is Permissible
• hu=(gz1g’z2)u=(gu)z1(g’u)z2=az1a’z2
variable substitution
variable substitution
distributive, commutative
• How can a “compiler” verify that
CCACCA1 is permissible?
– Variable substitution is easy
– Distributive, commutative rules would
have to be built into the tool
• Just like replacing x+y with y+x
June 2005
DDH
+DDH
TCR
+TCR
+t /q^4
CCA4
CCA1
+1/q
XYZ
+epsilon
CCA1
CCA5
CCA2
CCA[CS]
CCA0
CCA5’
CCA2
CCA3’
+2t / q
CCA4
CCA5
game with bad events
game with output
game that depends on a (binary) parameter
The empty game
game that is derived from template XYZ
transformation that changes the probability by epsilon
transformation that is justified by a reduction
June 2005
Game CCA2
• Replacing
with
12. u  {1,2,…,q}
13. a=gu, a’=g’u, b=az1a’z2, c=b·ms
12. u,u’  {1,2,…,q}
13. a=gu, a’=g’u’, b=az1a’z2, c=b·ms
• This sure changes the distribution
• We intend to show that if
Pr[CCA1(b,t)1], Pr[CCA2(b,t)1]
differ by some , then we can “break
DDH” in G with the same probability 
June 2005
The DDH Assumption
• No (efficient) algorithm distinguishes
(g,gx,gy,gxy) from (g,gx,gy,gz)
– Where gG, x,y,z{1,2,…q}
– Equivalent to saying that you cannot
distinguish (g,g’,gu,g’u) from (g,g’,gu,g’u’)
• This assumption underlies the security
of the Diffie-Hellman key-exchange
protocol
June 2005
Pseudo-code for DDH
DDH (parameter: bit s’)
201. g,g’G,
u,u’{1,2,…,q}
202. if s’=0 then a=gu, a’=g’u’
203. else a=gu, a’=g’u
204. guess=Distinguisher(g,g’,a,a’), Output guess
• The “DDH assumption” is that DDH=
|Pr[DDH(0)1]-Pr[DDH(1)1]| is
small for any efficient Distinguisher
June 2005
The Reduction
• Show that CCA1DDH(1),CCA2DDH(0)
are permissible transformations
• Instantiate the Distinguisher in DDH
(by morphing the code of CCA1/CCA2)
– Just moving pieces of code around
– A “compiler” can check that this is ok
• Only changing the order of “independent
statements”
June 2005
DDH
+DDH
TCR
+TCR
+t /q^4
CCA4
CCA1
+1/q
XYZ
+epsilon
CCA1
CCA5
CCA2
CCA[CS]
CCA0
CCA5’
CCA2
CCA3’
+2t / q
CCA4
CCA5
game with bad events
game with output
game that depends on a (binary) parameter
The empty game
game that is derived from template XYZ
transformation that changes the probability by epsilon
transformation that is justified by a reduction
June 2005
Bad Events
• Recall Dec(a,a’,c,d):
21. assert a,a’,c,d  G
22. v = H(a,a’,c)
23. assert d = ax1+vy1 a’x2+vy2
24. b = az1a’z2, m=c/b
25. Output m
• a,a’ are supposed to be gu,g’u
• It’s a bad thing if Attacker sends
(gu,g’u’,c,d) but line 23 passes
• How to represent bad events in code?
June 2005
Bad-event Flags
• A Boolean flag
• Initialized to false, only has
assignments to true in the code
• Designated as “interesting”
• Adding a bad-event flag is always a
permissible code-transformation
– Represens an argument that starts with
“let BAD be the event where…”
June 2005
After-bad-is-set-nothingmatters [BR04]
• Code that is executed only when
badFlag=true is treated as dead code
– Even if it effects other vars-of-interest
• Why?
– If badFlag=true then “all bets are off”,
no more vars-of-interest, all code is dead
– We intend to prove that badFlag=true
rarely ever happens
June 2005
Game CCA3
• Replace
with
g,g’G
gG, w{1,…q}, g’=gw
– The tool should have a rule for algebraic
groups saying that this is permissible
• Replace
with
23. assert d=ax1+vy1a’x2+vy // else fail
23.
d=ax1+vy1a’x2+vy2
a’aw
added
“dead code”
if
and
then badFlag=true, fail
23a. else assert d=ax1+vy1a’x2+vy2 // else fail
June 2005
Game CCA3’
• Quite a few other modifications
• But nothing that we didn’t see before
– Algebraic, logic manipulations
– Introducing new variables
– Code movement
• All made possible only after we
added the “dead code” in line 23
June 2005
DDH
+DDH
TCR
+TCR
+t /q^4
CCA4
CCA1
+1/q
XYZ
+epsilon
CCA1
CCA5
CCA2
CCA[CS]
CCA0
CCA5’
CCA2
CCA3’
+2t / q
CCA4
CCA5
game with bad events
game with output
game that depends on a (binary) parameter
The empty game
game that is derived from template XYZ
transformation that changes the probability by epsilon
transformation that is justified by a reduction
June 2005
Game CCA4
• Replace 13. … c=b·ms
By
13. … r{1,2,…,q}, c=gr
• Why is this permissible?
– Long story (four small steps)
– Trust me, it works
• CCA4 no longer depends on s, it is just
one game now (rather than two)
• Nothing to compare the output to
– So we no longer care about it, can removed it
June 2005
Eliminating the Output
• Started with two games with output
– The goal is to compare their outputs
• Morphed until their code is identical
– So their output must be identical
• Output is no longer “of interest”
– We are done analyzing the output, we
know that the difference is zero
– Eliminating it becomes permissible
June 2005
DDH
+DDH
TCR
+TCR
+t /q^4
CCA4
CCA1
+1/q
XYZ
+epsilon
CCA1
CCA5
CCA2
CCA[CS]
CCA0
CCA5’
CCA2
CCA3’
+2t / q
CCA4
CCA5
game with bad events
game with output
game that depends on a (binary) parameter
The empty game
game that is derived from template XYZ
transformation that changes the probability by epsilon
transformation that is justified by a reduction
June 2005
What’s Next?
• Game CCA4 still has bad flags, how
do we eliminate these?
• Either via reductions
– E.g., reduction to finding collisions in H
– I don’t have time to show it here
• Or via “probabilistic analysis”
– Example in the next slide
June 2005
Eliminating Bad Flags
• Consider the following code
Example(parameter: a) // a is an n-bit string
1. x  random-n-bit-string
2. if x=a then badFlagtrue
• Tool “knows” that
– Variable x is a “random n-bit string”
– Variables x and a are independent
• “Can deduce” that x=a has prob. 2-n
– So eliminating badFlag has penalty 2-n
June 2005
Eliminating Bad Flags (2)
• User tells the tool to eliminate the
designation of badFlag as bad flag
• Tool looks for a rule that bounds the
probability of badFlagtrue by some 
• If found, tool “eliminates badFlag”, records
penalty 
• Else, tool records an “impermissible
transformation”
– User proves on paper some 
June 2005
The Proof of CS98
DDH
+DDH
TCR
+TCR
+t /q^4
CCA5’
CCA4
CCA1
CCA2
+1/q
CCA[CS]
CCA
XYZ
+epsilon
CCA1
CCA5
CCA2
CCA3’
+2t / q
CCA4
CCA5
game with bad events
game with output
game that depends on a (binary) parameter
The empty game
game that is derived from template XYZ
transformation that changes the probability by epsilon
transformation that is justified by a reduction
June 2005
The Proof of CMC [HR03]
Mode-of-operation[CMC]
+(2mq)2 /2n,
see Eq (13), Page 21
£2 due to symmetry,
see Eq (12), Page 21
RND
+(mq)2 /2n
CMC
RND1
RND3
game with bad events
?
RND3’
NON1
?
NON2
game with output
The empty game
XYZ
+epsilon
?
game that is derived from template XYZ
transformation that changes the probability by epsilon
An impermissible transformation
June 2005
Building the Tool
June 2005
Four Major Components
• Engine: similar to optimizing compiler
– Parses statements, control-flow graph
– Handles variable substitution, code
movement, adding/removing “dead
code”, etc.
• Library of code-transformations
• Library of templates
• User interface
June 2005
Transformations Library
• Represent common arguments in
proofs
– Algebraic manipulations
– Rules to eliminate bad flags, output
– Other rules
• A community development effort?
– My proof uses an argument not in the
library, I code it up so others can use it
too
June 2005
Template Library
• Code templates, represent common
security goals and assumptions
• E.g., a template for DDH, a template
for CCA-security, etc.
• Also community development effort?
June 2005
User Interface
• Probably the hardest part
• Should be easy for people to write
their proofs using this tool
– Specify games
• “Sender proves to receiver in ZeroKnowledge that it knows the DL of x”
– Access common transformations
• Similarities to U.I. of development
environment?
June 2005
My Bottom Line
• It can be built, with a lot of work
– Perhaps similar to a new programming
language: compiler, run-time,
development environment, …
• Is there a “business case”?
– Where can I get resources to develop
this tool?
June 2005
Contact me if you
are interested in
working on this
June 2005