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