Previous Entry Share Next Entry
2016-01

ICFPC2013 и асимметричная криптография

tl;dr: задача ICFPC этого года эквивалентна построению универсальной ломалки для асимметричной криптографии (восстановить trapdoor-функцию с помощью chosen-plaintext атаки и оракула организаторов) вряд ли это intended, но забавно.

В связи с этим вопрос: есть ли вообще какие-либо статьи по применению SMT солверов для оптимизации решения discrete logarithm или factoring problem?

This entry was originally posted at http://wizzard.dreamwidth.org/298710.html. It has comment count unavailable comments. Please comment there using OpenID.

  • 1
_winnie August 10th, 2013
misread: с помощью chosen-plaintext атаки и подкупа организаторов

_winnie August 10th, 2013
intellince-атака: поискать пейперы организаторов :]
( я не знаю, будет ли полезно, но с некоторой вероятностью они будут петь то, над чем сами работают )

Edited at 2013-08-10 05:21 pm (UTC)

sassa_nf August 11th, 2013
methinks, любой профессор на каком-то этапе развлекается со студиками задачами на равенство двух функций.

wizzard0 August 11th, 2013
Ничего не могу прокомментировать.

sassa_nf August 11th, 2013
а как они, по-твоему, сравнивают, что присланный вариант функционально равен задуманному.

nponeccop August 12th, 2013
диспрувером равенства? их сколько угодно.

Edited at 2013-08-12 08:37 am (UTC)

sassa_nf August 12th, 2013
я думал в общем виде задача неразрешима

wizzard0 August 12th, 2013
ну условие почитай что ли, ссылка в теле поста есть

sassa_nf August 12th, 2013
я не знаю, что не понятно.

Было предложение почитать статьи организаторов. А я продолжаю бла-бла и замечаю, что статьи могут быть на обратную тему: участник отправляет вариант программы, а на том конце нужно делать что? Сравнить, равна ли эта программа задуманной функционально. Это как решить задачу проверки на равенство функций f(x) и g(x) или задать экстенсиональное равенство функций.

wizzard0 August 12th, 2013
Ну дык такие статьи есть, полно их.

nponeccop August 12th, 2013
"This is called the extensional view of functions, because it specifies that the only thing observable about a function is how it maps inputs to outputs"

Но в твоей задаче же не экстенсиональное равенство - о функциях известна структура.

Возьмите для сравнения хотя бы ЛИ. Равенство или неравенство любых термов, имеющих НФ, доказывается элементарно редукцией к НФ.

sassa_nf August 12th, 2013
и даже if0 x x (shr1 x) можно приравнять shr1 x?

wizzard0 August 12th, 2013
Естественно)
Например, Pex говорит, что эти две вещи эквивалентны -

public class Program 
{
    public static int Puzzle(int i)
    {
if(i==10) return 10;
return 5+(i>>1);
    }
}


и
public class Program 
{
    public static int Puzzle(int i)
    {
      if(divtest(i).HasValue) return divtest(i).Value;
return 5+(i>>1);
    }
    static int? divtest(int x){
      if(x==100) return 55;
      return null;
    }
}

sassa_nf August 12th, 2013
а такое:

public class Program 
{
    public static int Puzzle(int i)
    {
      if(!divtest(i).HasValue) return divtest(i+1).Value;
return 5+(i>>1);
    }
    static int? divtest(int x){
      if(x==100) return null;
      return 55;
    }
}

wizzard0 August 12th, 2013
такое "equal"

sassa_nf August 12th, 2013
а такое:

public class Program 
{
    public static int Puzzle(int i)
    {
      if(!divtest(i).HasValue) return 5;
return 5+divtest(i+2);
    }
    static int? divtest(int x){
      if(x==0) return null;
      return i-(i>>1)-1;
    }
}

wizzard0 August 12th, 2013
твоя функция а) не компилится)))

б) после добавления каста отличается (например, для i=1)

в) не тотальная (например, для i=-2)

sassa_nf August 12th, 2013
а я только что хотел поправить, т.к. нужно по индукции таки продемонстрировать:

    static int? divtest(int x){
      if(x==0) return null;
      return (x & -2)-(x>>1)-1;
    }
а функция таки тотальнаяну то есть да, вот добавь ещё проверку на -2 перед вызовом.


и вообще, примеры эти здесь для того, чтобы выяснить как это равенство доказывать с помощью редукции к НФ. По-моему, здесь без индукции по целым числам не обойтись.

Edited at 2013-08-12 02:04 pm (UTC)

wizzard0 August 12th, 2013
Puzzle(0x7FFFFFFE) -> 0xC0000004, а надо 0x40000004 ;)

продолжаем дальше, мне нравится))

> По-моему, здесь без индукции по целым числам не обойтись.

не исключено, что она там есть

Edited at 2013-08-12 02:13 pm (UTC)

sassa_nf August 12th, 2013
"а надо 0x40000004 ;)"

это почему у вас >> беззнаковый?

нудный ты :) заставляешь старика приседать только чтобы простую мысль донести, что дело не в НФ. перекастовать в long и всё будет путём.

Edited at 2013-08-12 02:28 pm (UTC)

wizzard0 August 12th, 2013
хороший вопрос, дебагаю)

wizzard0 August 12th, 2013
у тебя кстати скайп или другой IM есть?

(Deleted comment)
wizzard0 August 12th, 2013
"your messages will be seen later" вроде добавилось...

nponeccop August 12th, 2013
> что дело не в НФ. перекастовать в long

Я и не говорил, что дело не в НФ, перекастовать в long. Я всего лишь хотел узнать определения экстенсиональности и интенсиональности, которые ты используешь.

Edited at 2013-08-12 10:13 pm (UTC)

sassa_nf August 13th, 2013
ну у меня чёткого определения нет :) то, что ты цитируешь, меня устраивает. Я интенсиональность понимаю как синтаксическое равенство программ, а экстенсиональность - равенство выводов для всех вводов.

Меня также устраивают и твои аргументы - тут действительно известна структура обоих программ, поэтому уже совсем не сравнение чёрных ящиков (стало быть, не экстенсиональность). Для меня всё ещё загадка, как можно обойтись без индукции по числам, но вон антиламер цитирует важный вывод, хотя и не понятно, откуда это берётся. Конечно, двоичные деревья сравнивать просто - теперь бы ещё научиться программу в decision tree переводить.

Edited at 2013-08-13 02:06 pm (UTC)

sassa_nf August 12th, 2013
using System;

public class Program {
  public static int Puzzle(int x) {
    return x*(x+1)/2+x*(x-1);
  }
}


равно

using System;

public class Program {
  public static int Puzzle(int x) {
    if (x<2) return x;
    int s=x*x;
    while(x-->0) {
      s+=x--;
      if (x++==0) return s;
    }
    return 42;
  }
}


хотя очевидно, что на отрицательных числах это не верно.

wizzard0 August 12th, 2013
что-то тут не то

wizzard0 August 12th, 2013
кстати циклы и списки эта штуковина тоже поддерживает

antilamer August 13th, 2013
Такие функции, как указаны в условии, легко (conceptually) кодируются в OBDD (одна функция int64 -> int64 = 64 OBDD, каждая с 64 входами), у которых равенство тривиальное.

nponeccop August 12th, 2013
В общем виде действительно неразрешима, но это не важно :)

Неразрешимость ни о чём нам, промышленным программистам, не говорит. Она всего лишь запрещает строить a decision procedure which is both complete and sound.

Во-первых, это значит, что если задача неразрешима - к ней можно подбираться неполным алгоритмом или иногда ошибающимся (например, вероятностным) алгоритмом.

Во-вторых, если задача разрешима - то это вовсе не значит, что полной процедурой разрешения можно воспользоваться. Всё равно может потребоваться опять же incomplete or unsound polynomial approximation.

Чисто гипотетически, можно надеяться что для данного случая предикат равенства функций разрешим, но разрешимость нам ничего не даёт, см. выше.

Де факто у оргов разрешитель incomplete, но кол-во задач, для которых оракул ответил "не знаю" и зафейлил задачу, не предоставив контрпримера, оказалось ничтожно мало. Я не могу сейчас пруфлинка найти.

wizzard0 August 12th, 2013
В постановке от оргов задача разрешима, но NP.

Они писали, что там какие-то единицы задач не смогли сравнить за таймаут (20 секунд)

В доках на сам Z3 (на котором, полагаю, построен сервер оргов) написано, что есть масса эвристик, хаков и ограничений даже на разрешимые вещи, равно как и методы на часть неразрешимых ;)

thedeemon August 14th, 2013
На мои программы их сервер примерно в 0.5% случаев отвечал, что не может удостовериться в эквивалентности.

wizzard0 August 12th, 2013
http://www.pexforfun.com/ вот, играйся)

nponeccop August 12th, 2013
> эквивалентна построению универсальной ломалки

Отнюдь. Идея trapdoor в том, что её не восстановить по спецификации. Это скорее ломалка наивных шифров с security by obscurity, что-то вроде универсального кейгена (схемы генерации серийников почему-то редко используют научную криптографию).

> есть ли вообще какие-либо статьи

На гугле забанили?

https://www.google.com.ng/search?q=sat+solver+factorization

Edited at 2013-08-12 08:37 am (UTC)

wizzard0 August 12th, 2013
> Отнюдь
Nope.

Я утверждаю, что "найти неизвестную функцию" === "восстановить ключ известного trapdoor'a параметризованного неизвестным ключом"

nponeccop August 12th, 2013
Ну с этим я не спорю, разве что только в деталях (это не эквивалентность а односторонняя импликация).

Я спорю с тем, что использованных оргами примитивов скорее всего не хватит для построения трапдора. Т.е. задачи всего лишь похожи, но многое придется поменять.

wizzard0 August 12th, 2013
Векторы узковаты, да. А так вроде хватает, умножение и возведение в степень сделать можно.

  • 1
?

Log in

No account? Create an account