Nyan101 Blog

지난번 글에서는 이산 로그 문제에 대해 다뤘으니 이번에는 소인수분해 문제를 해결하는 알고리즘에 대해 알아보자. 코드는 이전과 마찬가지로 아래와 같은 수정이 들어간 파이썬 문법을 따랐다. 양 끝을 명시적으로 나타내기 위해 range(st, ed+1) 대신 [st...ed]와 같은 표기를 사용했다. 파이썬에서 거듭제곱을 나타내는 a**b 대신 일반적으로 사용되는 a^b 표기를 사용했다. 지난 이산 로그 문제와는...

암호학, 특히 공개키 기반 암호시스템은 주로 1)소인수분해 문제 혹은 2)이산 로그 문제를 기반으로 설계되는 경우가 많다. 그중 이산 로그 문제와 이를 해결하는 알고리즘에 대해 알아보자. 예시로 든 코드는 기본적으로 파이썬 문법을 따라 작성했으며 가독성을 위해 다음과 같은 부분을 수정했다. 파이썬에서 range(n)은 0부터 시작해 n이 아닌 n-1까지를 포함한다. 양 끝을 명시적으로...

얼마 전 코드포스에서 흥미로운 문제를 접했다. 대회 당시에는 풀지 못했는데, 에디토리얼을 읽어보던 중 뫼비우스 함수(Möbius function)에 대한 언급이 있어 이에 대해 좀더 자세히 알아보았다. Möbius function의 정의 뫼비우스 함수(Möbius function)는 자연수 n에 대해 다음과 같이 정의된다. (\(p\)는 소수) \[\mu(n) = \begin{cases} (-1)^k & \mathrm{if\,\,\,\,} n=p_1p_2\cdots p_k \, (p_i \neq p_j)\\...

대부분의 reference가 그렇듯이 읽다보면 쉽게 지루해진다. 지루함을 덜하고 Coq에 익숙해지기 위해 일단 예제를 조금씩 따라해보면서 익혀가기로 했다. 자바를 처음 배울 때 public static void main(int argv, char **argc)가 정확히 뭔지는 몰라도 “Hello World” 부터 찍어보는 그런 마음으로 진행해봤다. CoqIDE 실행 프로그램을 처음 실행하면 다음과 같은 화면을 볼 수 있다. 크게...

<Interactive Theorem Proving and Program Development>라는 책을 추천받아 조금씩 읽어보기로 했다. 첫 장에서는 Coq에 대한 간단한 안내를 진행한다. 책의 순서를 따라가면서 하나씩 알아보자 타입 먼저 Coq에서는 Gallina라는 언어를 사용해 요구사항(Specification)을 서술한다. 대부분의 다른 프로그래밍 언어들과 마찬가지로 타입은 declaration과 typing rule에 의해 정해진다. declaration : type Z 에 대해 이 타입의...

이번 SCTF(Samsung CTF)의 700점짜리 문제로 튜링머신 설계가 나왔다. 총 4개의 문제 중 3개는 일반적인 오토마타 교과서에서 다루는 언어들(ex: \(L=\{ 0^n1^n | n \geq 0 \}\))이었지만 마지막 단계인 \(L=\{0^p | p \, \mathrm{\,is\,prime}\}\)가 다소 많은 시간을 잡아먹었다. 사실상 소수 판별을 하는 튜링 머신을 설계하라는 문제였는데, 기억상 다른 교재들에서도 이에 대한 명확한...