forked from crypto-agda/crypto-agda
-
Notifications
You must be signed in to change notification settings - Fork 0
/
README.agda
60 lines (48 loc) · 1.65 KB
/
README.agda
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
module README where
-- A module for bit-vectors which is used almost
-- everywhere in this development.
open import Data.Bits
open import elgamal
open import schnorr
open import generic-zero-knowledge-interactive
open import sum-properties
-- Randomized programs
open import flipbased
open import flipbased-counting
open import flipbased-running
open import flipbased-implem
open import flipbased-tree
-- A distance between randomized programs
open import program-distance
-- Pure guessing game, a game in which no strategy can
-- consistently win or consistently lose.
open import bit-guessing-game
-- Cryptographic pseudo-random generator game.
open import prg
-- “One time Semantic Security” of the “One time pad” cipher
-- on one bit messages. In other words, “xor”ing any bit with
-- a random bit will look random as well.
open import single-bit-one-time-pad
-- Ciphers, the “one time Semantic Security” game.
open import one-time-semantic-security
-- A simple reduction on ciphers.
open import composition-sem-sec-reduction
-- Tracking space and time through a restricted universe
-- of functions.
open import data-universe
open import fun-universe
open import agda-fun-universe
open import bits-fun-universe
open import fin-fun-universe
open import const-fun-universe
open import cost-fun-universe
open import inverse-fun-universe
open import circuit-fun-universe
open import syntax-fun-universe
-- TODO: Fix & restore the product of universes and ops
-- Draft modules of previous attempts.
-- There is still some code to rescue.
open import circuit
open import flipbased-tree-probas
open import flipbased-no-split
open import flipbased-product-implem