Sumário
Introdução
Abordagem
PRP/PRF Switching Lemma
Sintaxe
Técnicas de reescrita (transformação)
Prova Elementar para CBC MAC
The Game-Playing Technique
Marcelo Correia Pinheiro
Universidade do Vale do Rio dos Sinos
Teoria da Informação
Prof. Ernesto Lindstaedt
14 de junho de 2007
Marcelo Correia Pinheiro
The Game-Playing Technique
Sumário
Introdução
Abordagem
PRP/PRF Switching Lemma
Sintaxe
Técnicas de reescrita (transformação)
Prova Elementar para CBC MAC
1
2
3
4
4
5
6
Sumário
Introdução
O que é?
Abordagem
Como funciona?
PRP/PRF Switching Lemma
Provando o lema
Sintaxe
Executando um jogo
Cálculo da Probabilidade
Lema fundamental dos jogos
Técnicas de reescrita (transformação)
Depois de bad ser true, nada importa
Coin fixing
Lazy sampling
Prova Elementar para CBC MAC
Algoritmo
Teorema
Marcelo Correia Pinheiro
The Game-Playing Technique
Sumário
Introdução
Abordagem
PRP/PRF Switching Lemma
Sintaxe
Técnicas de reescrita (transformação)
Prova Elementar para CBC MAC
O que é?
É uma técnica baseada na utilização de “jogos” em pseudo-código,
cuja vantagem do adversário em atacar uma construção
criptográfica é calculada sobre a probabilidade que este jogo
atribua uma flag chamada bad como true. A probabilidade é
incrementada através de uma seqüência de modificações no
pseudo-código que levam a uma cadeia de jogos, até que a flag
bad seja atribuı́da.
Marcelo Correia Pinheiro
The Game-Playing Technique
Sumário
Introdução
Abordagem
PRP/PRF Switching Lemma
Sintaxe
Técnicas de reescrita (transformação)
Prova Elementar para CBC MAC
Como funciona?
Suponha a necessidade de calcular a vantagem de um adversário A
em atacar uma construção criptográfica. Essa vantagem é obtida
através da probabilidade (um número n ∈ < entre 0 e 1)
computada através da diferença entre as probabilidades de que A
retorne 1 em dois diferentes “mundos”. Sejam os seguintes passos:
Marcelo Correia Pinheiro
The Game-Playing Technique
Sumário
Introdução
Abordagem
PRP/PRF Switching Lemma
Sintaxe
Técnicas de reescrita (transformação)
Prova Elementar para CBC MAC
Como funciona?
Um pseudo-código - um jogo - é criado, obtendo os
comportamentos do mundo 1. Este jogo inicializa variáveis, interage
com o adversário e executa seu código.
Marcelo Correia Pinheiro
The Game-Playing Technique
Sumário
Introdução
Abordagem
PRP/PRF Switching Lemma
Sintaxe
Técnicas de reescrita (transformação)
Prova Elementar para CBC MAC
Como funciona?
Um pseudo-código - um jogo - é criado, obtendo os
comportamentos do mundo 1. Este jogo inicializa variáveis, interage
com o adversário e executa seu código.
Outro pseudo-código - um segundo jogo - é escrito, capturando os
comportamentos do mundo 0. Os pseudo-códigos dos jogos 1 e 0
são sintaticamente idênticos, com exceção do código que seta bad
para true.
Marcelo Correia Pinheiro
The Game-Playing Technique
Sumário
Introdução
Abordagem
PRP/PRF Switching Lemma
Sintaxe
Técnicas de reescrita (transformação)
Prova Elementar para CBC MAC
Como funciona?
Um pseudo-código - um jogo - é criado, obtendo os
comportamentos do mundo 1. Este jogo inicializa variáveis, interage
com o adversário e executa seu código.
Outro pseudo-código - um segundo jogo - é escrito, capturando os
comportamentos do mundo 0. Os pseudo-códigos dos jogos 1 e 0
são sintaticamente idênticos, com exceção do código que seta bad
para true.
Aplica-se o lema fundamental dos jogos para calcular, na presente
configuração dos jogos, a vantagem do adversário limitada na
probabilidade de bad ser atribuı́da em outro jogo.
Marcelo Correia Pinheiro
The Game-Playing Technique
Sumário
Introdução
Abordagem
PRP/PRF Switching Lemma
Sintaxe
Técnicas de reescrita (transformação)
Prova Elementar para CBC MAC
Como funciona?
Um pseudo-código - um jogo - é criado, obtendo os
comportamentos do mundo 1. Este jogo inicializa variáveis, interage
com o adversário e executa seu código.
Outro pseudo-código - um segundo jogo - é escrito, capturando os
comportamentos do mundo 0. Os pseudo-códigos dos jogos 1 e 0
são sintaticamente idênticos, com exceção do código que seta bad
para true.
Aplica-se o lema fundamental dos jogos para calcular, na presente
configuração dos jogos, a vantagem do adversário limitada na
probabilidade de bad ser atribuı́da em outro jogo.
Se escolhe um dos dois jogos e aplica-se pequenas transformações
no código, de forma a aumentar ou manter inalterada a
probabilidade de bad ser atribuı́da.
Marcelo Correia Pinheiro
The Game-Playing Technique
Sumário
Introdução
Abordagem
PRP/PRF Switching Lemma
Sintaxe
Técnicas de reescrita (transformação)
Prova Elementar para CBC MAC
Como funciona?
Um pseudo-código - um jogo - é criado, obtendo os
comportamentos do mundo 1. Este jogo inicializa variáveis, interage
com o adversário e executa seu código.
Outro pseudo-código - um segundo jogo - é escrito, capturando os
comportamentos do mundo 0. Os pseudo-códigos dos jogos 1 e 0
são sintaticamente idênticos, com exceção do código que seta bad
para true.
Aplica-se o lema fundamental dos jogos para calcular, na presente
configuração dos jogos, a vantagem do adversário limitada na
probabilidade de bad ser atribuı́da em outro jogo.
Se escolhe um dos dois jogos e aplica-se pequenas transformações
no código, de forma a aumentar ou manter inalterada a
probabilidade de bad ser atribuı́da.
Assim obtém-se uma cadeia de jogos, terminando com algum jogo
terminal, onde obtém-se a probabilidade da flag bad ser atribuı́da.
Marcelo Correia Pinheiro
The Game-Playing Technique
Sumário
Introdução
Abordagem
PRP/PRF Switching Lemma
Sintaxe
Técnicas de reescrita (transformação)
Prova Elementar para CBC MAC
Como funciona?
Cada jogo G é composto por uma tupla de programas, cada um
escrito numa linguagem de programação. Ambos os programas
possuem um conjunto comum de variáveis globais e locais, sendo
idênticos até a atribuição da variável bad.
Marcelo Correia Pinheiro
The Game-Playing Technique
Sumário
Introdução
Abordagem
PRP/PRF Switching Lemma
Sintaxe
Técnicas de reescrita (transformação)
Prova Elementar para CBC MAC
Provando o lema
Seja Perm(n) o conjunto de todas as permutações de {0, 1}n , e
Rand(n) o conjunto de todas as funções de {0, 1}n para {0, 1}n .
Para Af ⇒ 1 denota-se o evento do adversário A, utilizando um
oráculo f , retorna um bit de saı́da com valor 1. Assume-se que π
seja extraı́do randomicamente de Perm(n) e ρ seja selecionado de
Rand(n).
Lema
Seja n ≥ 1 um inteiro. Seja A um adversário que pergunta após q
consultas ao oráculo. Então |Pr [Aπ ⇒ 1]| − Pr [Aρ ⇒ 1]| ≤ q(q−1)
.
2n+1
Marcelo Correia Pinheiro
The Game-Playing Technique
Sumário
Introdução
Abordagem
PRP/PRF Switching Lemma
Sintaxe
Técnicas de reescrita (transformação)
Prova Elementar para CBC MAC
Marcelo Correia Pinheiro
Provando o lema
The Game-Playing Technique
Sumário
Introdução
Abordagem
PRP/PRF Switching Lemma
Sintaxe
Técnicas de reescrita (transformação)
Prova Elementar para CBC MAC
Provando o lema
Para provar o lema utilizando uma cadeia de jogos, seja o seguinte
cenário: múltiplas respostas à consultas A estão rodando em um
de dois jogos. Considere a interação de A com Game S1 ao invés
de interar com a permutação randômica π ← Perm(n), e da
mesma forma a interação de A com Game S1 no lugar de interar
com a função randômica do oráculo ρ ← Rand(n). Cada jogo é
sintaticamente idêntico, com exceção de Game S0, que não possui
a atribuição bad = true.
Marcelo Correia Pinheiro
The Game-Playing Technique
Sumário
Introdução
Abordagem
PRP/PRF Switching Lemma
Sintaxe
Técnicas de reescrita (transformação)
Prova Elementar para CBC MAC
Provando o lema
Como Game S0 simula a função randômica ρ ← Rand(n), temos
que Pr [Aρ ⇒ 1] = Pr [AS0 ⇒ 1]. Similarmente, ao verificar Game
S1, obtém-se Pr [Aπ ⇒ 1] = Pr [AS1 ⇒ 1]. Logo, reescrevendo
parcialmente a fórmula chega-se a
|Pr [Aπ ⇒ 1] − Pr [Aρ ⇒ 1]| = |Pr [AS1 ⇒ 1] − Pr [AS0 ⇒ 1]|.
Marcelo Correia Pinheiro
The Game-Playing Technique
Sumário
Introdução
Abordagem
PRP/PRF Switching Lemma
Sintaxe
Técnicas de reescrita (transformação)
Prova Elementar para CBC MAC
Provando o lema
Para calcular a probabilidade de atribuição da variável bad com as
alterações realizadas, seja a seguinte fórmula:
|Pr [AS1 ⇒ 1] − Pr [AS0 ⇒ 1]| ≤ Pr [AS0 setar bad]. Essa
transformação resulta no lema fundamental dos jogos. Esse lema
diz que, quando dois jogos são escritos e são sinteticamente iguais
até a atribuição da variável bad, a diferença das probabilidades que
A retorna 1 nos dois jogos é limitada pela probabilidade que bad é
atribuı́da no outro jogo.
Marcelo Correia Pinheiro
The Game-Playing Technique
Sumário
Introdução
Abordagem
PRP/PRF Switching Lemma
Sintaxe
Técnicas de reescrita (transformação)
Prova Elementar para CBC MAC
Executando um jogo
Cálculo da Probabilidade
Lema fundamental dos jogos
Um programa P é uma seqüência finita de instruções escritas em
alguma linguagem de programação L. Cada programa será
identificado pelo sua árvore sintática. Estes programas possuem
todas as construções de uma linguagem procedural: variáveis,
atribuições, instruições if, for, etc. Seja a seguinte definição:
Jogos
Um jogo G = ( Inicializa, P1 , P2 , ..., Pn , Finaliza) é uma
seqüência de programas.
Marcelo Correia Pinheiro
The Game-Playing Technique
Sumário
Introdução
Abordagem
PRP/PRF Switching Lemma
Sintaxe
Técnicas de reescrita (transformação)
Prova Elementar para CBC MAC
Marcelo Correia Pinheiro
Executando um jogo
Cálculo da Probabilidade
Lema fundamental dos jogos
The Game-Playing Technique
Sumário
Introdução
Abordagem
PRP/PRF Switching Lemma
Sintaxe
Técnicas de reescrita (transformação)
Prova Elementar para CBC MAC
Executando um jogo
Cálculo da Probabilidade
Lema fundamental dos jogos
Um adversário é um algoritmo probabilı́stico com a habilidade de
consultar algum número n ≥ 0 de oráculos, normalmente descrito
como um programa. O par de um jogo G e um adversário A é
chamado de jogo em execução, denotados normalmente como GA
ou AG .
Marcelo Correia Pinheiro
The Game-Playing Technique
Sumário
Introdução
Abordagem
PRP/PRF Switching Lemma
Sintaxe
Técnicas de reescrita (transformação)
Prova Elementar para CBC MAC
Executando um jogo
Cálculo da Probabilidade
Lema fundamental dos jogos
Inı́cio do jogo
Para rodar G = (Inicializa, P1 , P2 , ..., Pn , Finaliza) com A e uma
string de parâmetro param, inicializa-se invocando o programa
Inicializa enviando o parâmetro param. Então se roda A, passando
qualquer valor de retorno produzido por Inicializa para P1 .
Marcelo Correia Pinheiro
The Game-Playing Technique
Sumário
Introdução
Abordagem
PRP/PRF Switching Lemma
Sintaxe
Técnicas de reescrita (transformação)
Prova Elementar para CBC MAC
Executando um jogo
Cálculo da Probabilidade
Lema fundamental dos jogos
Execução intermediária
Quando o adversário A chama seu i esimo oráculo dada uma string,
essa string é informada ao programa Pi e este é executado. O
adversário A volta a ser executado quando Pi retorna a string
resultante.
Marcelo Correia Pinheiro
The Game-Playing Technique
Sumário
Introdução
Abordagem
PRP/PRF Switching Lemma
Sintaxe
Técnicas de reescrita (transformação)
Prova Elementar para CBC MAC
Executando um jogo
Cálculo da Probabilidade
Lema fundamental dos jogos
Término do jogo
Quando Pn termina sua execução, o método Finaliza é executado,
recebendo como parâmetro a string resultante da execução do
adversário A.
Marcelo Correia Pinheiro
The Game-Playing Technique
Sumário
Introdução
Abordagem
PRP/PRF Switching Lemma
Sintaxe
Técnicas de reescrita (transformação)
Prova Elementar para CBC MAC
Executando um jogo
Cálculo da Probabilidade
Lema fundamental dos jogos
Seja Pr [GA ⇒ 1] a probabilidade de que o resultado do jogo G seja
1 quando roda-se Ga . Diz-se que os jogos G e H são equivalentes
se, para qualquer adversário A, tem-se que
Pr [GA ⇒ 1] = Pr [HA ⇒ 1].
Define-se Pr [AG ⇒ 1] como a probabilidade do adversário A
retorne 1 quando se roda Ga . A vantagem de A em distingüir jogos
G
H
G e H é o número real AdvGdist
,H (A) = Pr [A ⇒ 1] − Pr [A ⇒ 1].
Diz-se que os jogos G e H são indistinguı́veis se, para qualquer
adversário A, obtém-se a igualdade Pr [AG ⇒ 1] = Pr [AH ⇒ 1].
Marcelo Correia Pinheiro
The Game-Playing Technique
Sumário
Introdução
Abordagem
PRP/PRF Switching Lemma
Sintaxe
Técnicas de reescrita (transformação)
Prova Elementar para CBC MAC
Executando um jogo
Cálculo da Probabilidade
Lema fundamental dos jogos
Lema fundamental
Sejam G e H jogos sintaticamente idênticos, e A um adversário.
Então Pr [GA ⇒ 1] − Pr [HA ⇒ 1] ≤ Pr [GA setar bad].
Marcelo Correia Pinheiro
The Game-Playing Technique
Sumário
Introdução
Abordagem
PRP/PRF Switching Lemma
Sintaxe
Técnicas de reescrita (transformação)
Prova Elementar para CBC MAC
Depois de bad ser true, nada importa
Coin fixing
Lazy sampling
Há algumas técnicas úteis na transformação de jogos, de forma a
aumentar ou manter a probabilidade da flag bad ser atribuı́da.
Destacam-se:
Depois de bad ser atribuı́da, nada mais importa
Marcelo Correia Pinheiro
The Game-Playing Technique
Sumário
Introdução
Abordagem
PRP/PRF Switching Lemma
Sintaxe
Técnicas de reescrita (transformação)
Prova Elementar para CBC MAC
Depois de bad ser true, nada importa
Coin fixing
Lazy sampling
Há algumas técnicas úteis na transformação de jogos, de forma a
aumentar ou manter a probabilidade da flag bad ser atribuı́da.
Destacam-se:
Depois de bad ser atribuı́da, nada mais importa
Coin fixing
Marcelo Correia Pinheiro
The Game-Playing Technique
Sumário
Introdução
Abordagem
PRP/PRF Switching Lemma
Sintaxe
Técnicas de reescrita (transformação)
Prova Elementar para CBC MAC
Depois de bad ser true, nada importa
Coin fixing
Lazy sampling
Há algumas técnicas úteis na transformação de jogos, de forma a
aumentar ou manter a probabilidade da flag bad ser atribuı́da.
Destacam-se:
Depois de bad ser atribuı́da, nada mais importa
Coin fixing
Lazy sampling
Marcelo Correia Pinheiro
The Game-Playing Technique
Sumário
Introdução
Abordagem
PRP/PRF Switching Lemma
Sintaxe
Técnicas de reescrita (transformação)
Prova Elementar para CBC MAC
Depois de bad ser true, nada importa
Coin fixing
Lazy sampling
Após a flag bad ser atribuı́da com true, pode-se remover os
trechos conseguintes de código do programa ou simplesmente
mantê-los; a probabilidade será inalterada.
Depois de bad ser true, nada importa
Sejam G e H jogos sintaticamente idênticos e A um adversário.
Então Pr [GA setar bad] = Pr [HA setar bad].
Marcelo Correia Pinheiro
The Game-Playing Technique
Sumário
Introdução
Abordagem
PRP/PRF Switching Lemma
Sintaxe
Técnicas de reescrita (transformação)
Prova Elementar para CBC MAC
Depois de bad ser true, nada importa
Coin fixing
Lazy sampling
Suponha que um jogo GA possua as seguintes caracterı́sticas: um
oráculo P cujo parâmetro de entrada input informado por A esteja
vazio e o resultado também seja vazio. Esse jogo conterá uma flag
bad. A seguir o adversário A solicita, em seqüência, exatas q
strings de consulta para P, onde o programa armazena em
variáveis X1 , ..., Xq tais strings de entrada; o resultado dessas
strings é armazenado em variáveis Y1 , ..., Yq . Seja então C um
conjunto de tuplas (X1 , ..., Xq , Y1 , ..., Yq ) onde cada vetor de
consultas X1 , ..., Xq e suas respostas Y1 , ..., Yq podem ocorrer na
execução de GA em C . Este conjunto é denominado conjunto de
consulta/resposta para GA .
Marcelo Correia Pinheiro
The Game-Playing Technique
Sumário
Introdução
Abordagem
PRP/PRF Switching Lemma
Sintaxe
Técnicas de reescrita (transformação)
Prova Elementar para CBC MAC
Depois de bad ser true, nada importa
Coin fixing
Lazy sampling
Seja γ o conjunto de todas as variáveis Y ∈
/ {X1 , ..., Xq , Y1 , ..., Yq }
em um jogo G para cada Yi . Diz-se que GA é ignorado se a
variável bad não depende de qualquer variável de γ, ou seja,
nenhuma variável Yi influencia na computação de bad.
Marcelo Correia Pinheiro
The Game-Playing Technique
Sumário
Introdução
Abordagem
PRP/PRF Switching Lemma
Sintaxe
Técnicas de reescrita (transformação)
Prova Elementar para CBC MAC
Depois de bad ser true, nada importa
Coin fixing
Lazy sampling
Com um jogo ignorado GA , um conjunto consulta/resposta C para
GA e um ponto Q = (X1 , ..., Xq , Y1 , ..., Yq ) ∈ C , forma-se um novo
jogo H C , semelhante à G exceto pelo fato de não ter um oráculo
P.
Seja H = CoinFixAC (G ) de H C para o primeiro item Q ∈ C que
maximiza Pr [HAC setar bad]. Como HA não depende de A, pode-se
omitı́-lo e assim ainda ter um jogo em execução.
Marcelo Correia Pinheiro
The Game-Playing Technique
Sumário
Introdução
Abordagem
PRP/PRF Switching Lemma
Sintaxe
Técnicas de reescrita (transformação)
Prova Elementar para CBC MAC
Depois de bad ser true, nada importa
Coin fixing
Lazy sampling
Técnica Coin-fixing
Seja GA um jogo ignorado que possua um conjunto C do tipo
consulta/resposta. Seja H = CoinFixAC (G ). Então
Pr [GA setar bad] ≤ Pr [H setar bad].
Marcelo Correia Pinheiro
The Game-Playing Technique
Sumário
Introdução
Abordagem
PRP/PRF Switching Lemma
Sintaxe
Técnicas de reescrita (transformação)
Prova Elementar para CBC MAC
Depois de bad ser true, nada importa
Coin fixing
Lazy sampling
Ao invés de realizar escolhas a cada transformação, pode ser
conveniente reescrever o jogo prorrogando essas escolhar até o
momento ideal. Considere o seguinte exemplo: seja um jogo que
interage com um adversário utilizando uma permutação randômica
π em n bits. Uma forma de montar esse jogo seria escolher π
randomicamente de Perm(n) durante a função Inicializa e então,
quando solicitada uma consulta X ∈ {0, 1}n , retorna π(X ). A
alternativa tardia para implementar π seria começar com uma
permutação parcial de π de n bits para n bits, todos indefinidos.
Quando solicitada uma consulta X ainda não pertencente ao
domı́nio de π, o oráculo pode escolher um valor Y randomicamente
da escala de π, definindo π(X ) ← Y , e retornando Y .
Marcelo Correia Pinheiro
The Game-Playing Technique
Sumário
Introdução
Abordagem
PRP/PRF Switching Lemma
Sintaxe
Técnicas de reescrita (transformação)
Prova Elementar para CBC MAC
Algoritmo
Teorema
Seja o seguinte algoritmo para o cifrador CBC:
Algoritmo CBC
Parse M as M1 ..Mm
C0 ← 0 n
for i ← 1 to m do Ci ← Ci−1 ⊕ Mi
return Cm
Marcelo Correia Pinheiro
The Game-Playing Technique
Sumário
Introdução
Abordagem
PRP/PRF Switching Lemma
Sintaxe
Técnicas de reescrita (transformação)
Prova Elementar para CBC MAC
Algoritmo
Teorema
Seja Perm(n) a notação do conjunto de todas as permutações em
{0, 1}n e Rand(mn, n) a notação do conjunto de todas as funções
de {0, 1}mn para {0, 1}n . Para m ≥ 1 e π ∈ Perm(n) seja CBCm
π a
n
mn
restrição de CBC para o domı́nio {0, 1} . Tendo um algoritmo
A com um oráculo de acesso para a função F : {0, 1}mn ← {0,
1}n , seja
m
$
CBCπ (.) ⇒ 1] − Pr [ρ ←$
Advcbc
n,m (A) = Pr [π ← Perm(n): A
Rand(mn, n): Aρ(.) ⇒ 1]
a notação da vantagem de A. Então
n
o
cbc (A)
Advcbc
(q)
=
max
Adv
n,m
n,m
denota o máximo que todos os adversários A solicitam até q
consultas.
Marcelo Correia Pinheiro
The Game-Playing Technique
Sumário
Introdução
Abordagem
PRP/PRF Switching Lemma
Sintaxe
Técnicas de reescrita (transformação)
Prova Elementar para CBC MAC
Algoritmo
Teorema
CBC MAC
Suponha m, q ≥ 2 e n ≥ 1. Então
Advcbc
n,m (q) ≤
Marcelo Correia Pinheiro
m2 q 2
2n
The Game-Playing Technique
Sumário
Introdução
Abordagem
PRP/PRF Switching Lemma
Sintaxe
Técnicas de reescrita (transformação)
Prova Elementar para CBC MAC
Algoritmo
Teorema
Figura do paper!
Marcelo Correia Pinheiro
The Game-Playing Technique
Sumário
Introdução
Abordagem
PRP/PRF Switching Lemma
Sintaxe
Técnicas de reescrita (transformação)
Prova Elementar para CBC MAC
Algoritmo
Teorema
M. Bellare e P. Rogaway, The Game-Playing Technique. 11 de
Dezembro de 2004.
http://inf.unisinos.br/∼linds/teoinfo/bellare04gameplaying.pdf
Marcelo Correia Pinheiro
The Game-Playing Technique
Download

The Game-Playing Technique