Changes in preparation for HACS

Qcode · Qcode · commit 79d56373e001 · 2024-03-12T14:32:01.000-04:00
diff --git a/.gitignore b/.gitignore
@@ -13,3 +13,5 @@ _site/
 # Ignore folders generated by Bundler
 .bundle/
 vendor/
+
+**/.DS_Store
diff --git a/Gemfile b/Gemfile
@@ -5,3 +5,7 @@ gem "jekyll", "~> 4.3.3" # installed by `gem jekyll`
 
 gem "just-the-docs", "0.8.1" # pinned to the current release
 # gem "just-the-docs"        # always download the latest release
+
+group :jekyll_plugins do
+  gem 'jekyll-katex'
+end
diff --git a/Gemfile.lock b/Gemfile.lock
@@ -9,6 +9,7 @@ GEM
       eventmachine (>= 0.12.9)
       http_parser.rb (~> 0)
     eventmachine (1.2.7)
+    execjs (2.9.1)
     ffi (1.16.3)
     forwardable-extended (2.6.0)
     google-protobuf (3.25.3-arm64-darwin)
@@ -34,6 +35,9 @@ GEM
       webrick (~> 1.7)
     jekyll-include-cache (0.2.1)
       jekyll (>= 3.7, < 5.0)
+    jekyll-katex (1.0.0)
+      execjs (~> 2.7)
+      jekyll (>= 3.6, < 5.0)
     jekyll-sass-converter (3.0.0)
       sass-embedded (~> 1.54)
     jekyll-seo-tag (2.8.0)
@@ -80,6 +84,7 @@ PLATFORMS
 DEPENDENCIES
   jekyll (~> 4.3.3)
   just-the-docs (= 0.8.1)
+  jekyll-katex
 
 BUNDLED WITH
    2.3.26
diff --git a/_config.yml b/_config.yml
@@ -6,3 +6,6 @@ url: https://just-the-docs.github.io
 
 aux_links:
   ProofFrog Hub: https://github.com/ProofFrog
+
+plugins:
+  - jekyll-katex
diff --git a/_includes/head_custom.html b/_includes/head_custom.html
@@ -0,0 +1 @@
+<link rel="stylesheet" href="https://cdn.jsdelivr.net/npm/katex@0.11.1/dist/katex.min.css" integrity="sha384-zB1R0rpPzHqg7Kpt0Aljp8JPLqbXI3bhnPWROx27a9N0Ll6ZP/+DiW/UqRcLbRjq" crossorigin="anonymous">
diff --git a/assets/diagram.png b/assets/diagram.png
diff --git a/examples.md b/examples.md
@@ -0,0 +1,78 @@
+---
+title: Examples
+layout: default
+---
+
+# Examples
+
+Below are a list of examples that ProofFrog can currently verify.
+Many are adapted from [The Joy of Cryptography](https://joyofcryptography.com/).
+In such cases, we will indicate which claim in the textbook is being proved.
+
+## One-Time Uniform Ciphertexts implies One-Time Secrecy
+
+This proves [Theorem 2.15](https://joyofcryptography.com/pdf/book.pdf#page=49).
+
+The proof file can be found [here](https://github.com/ProofFrog/examples/blob/main/Proofs/SymEnc/OTUC%3D%3EOTS.proof).
+
+## CPA$ Security implies CPA Security
+
+This proves [Claim 7.3](https://joyofcryptography.com/pdf/book.pdf#page=145)
+
+The proof file can be found [here](https://github.com/ProofFrog/examples/blob/main/Proofs/SymEnc/CPA%24%3D%3ECPA.proof).
+
+## Composing Two Symmetric Encryption Schemes for One-Time Uniform Ciphertexts
+
+This proof analyzes a symmetric encryption scheme {% katex %}\Sigma{% endkatex %} that composes two symmetric encryption schemes {% katex %}S{% endkatex %} and {% katex %}T{% endkatex %} where {% katex %}S.C = T.M{% endkatex %}, and
+{% katex display %}
+\Sigma.\mathrm{KeyGen}() = (S.\mathrm{KeyGen()}, T.\mathrm{KeyGen()})
+{% endkatex %}
+{% katex display %}
+\Sigma.\mathrm{Enc}((k_S, k_T), m) = T.\mathrm{Enc}(k_T, S.\mathrm{Enc}(k_S, m))
+{% endkatex %}
+{% katex display %}
+\Sigma.\mathrm{Dec}((k_S, k_T), c) = S.\mathrm{Dec}(k_S, T.\mathrm{Dec}(k_T, c))
+{% endkatex %}
+
+If {% katex %}T{% endkatex %} has one-time uniform ciphertexts, then so does {% katex %}\Sigma{% endkatex %}. The proof file can be found [here](https://github.com/ProofFrog/examples/blob/main/Proofs/SymEnc/GeneralDoubleOTUC.proof)
+
+## Composing Two Symmetric Encryption Schemes for CPA$ security
+
+This proof analyzes the same encryption scheme {% katex %}\Sigma{% endkatex %} as in the prior heading. If {% katex %}T{% endkatex %} is CPA$ secure, then so is {% katex %}\Sigma{% endkatex %}. The proof file can be found [here](https://github.com/ProofFrog/examples/blob/main/Proofs/SymEnc/DoubleCPA%24.proof).
+
+
+## Double One-Time Pad has One-Time Uniform Ciphertexts
+
+This proves [Claim 2.13](https://joyofcryptography.com/pdf/book.pdf#page=45).
+
+The proof file can be found [here](https://github.com/ProofFrog/examples/blob/main/Book/2/2_13.proof).
+
+## Pseudo One-Time Pad has One-Time Uniform Ciphertexts
+
+This proves [Claim 5.4](https://joyofcryptography.com/pdf/book.pdf#page=102)
+
+The proof file can be found [here](https://github.com/ProofFrog/examples/blob/main/Book/5/5_3.proof).
+
+## Pseudorandomness of a length-tripling PRG
+
+This proves [Claim 5.5](https://joyofcryptography.com/pdf/book.pdf#page=105)
+
+The proof file can be found [here](https://github.com/ProofFrog/examples/blob/main/Proofs/PRG/TriplingPRGSecure.proof).
+
+## One-Time Secrecy implies CPA Security for Public Key Encryption Schemes
+
+This proves [Claim 15.5](https://joyofcryptography.com/pdf/book.pdf#page=273)
+
+The proof file can be found [here](https://github.com/ProofFrog/examples/blob/main/Proofs/PubEnc/OTS%3D%3ECPA.proof).
+
+## Hybrid Encryption is CPA secure
+
+This proves [Claim 15.9](https://joyofcryptography.com/pdf/book.pdf#page=279)
+
+The proof file can be found [here](https://github.com/ProofFrog/examples/blob/main/Proofs/PubEnc/Hybrid.proof).
+
+## Encrypt-then-MAC is CCA secure
+
+This proves [Claim 10.10](https://joyofcryptography.com/pdf/book.pdf#page=205)
+
+The proof file can be found [here](https://github.com/ProofFrog/examples/blob/main/Proofs/SymEnc/EncryptThenMACCCA.proof).
diff --git a/files/game.md b/files/game.md
@@ -0,0 +1,42 @@
+---
+title: Game Files
+layout: default
+parent: Files
+nav_order: 3
+---
+
+# Game Files
+
+Game files allow the user to specify security definitions in the form of a pair of games that must be proved indistinguishable.
+Each function listed in a game is provided implicitly to the adversary in the form of an oracle.
+Games may also contain private state that is maintained between oracle calls.
+Finally, each game has the option to specify an `Initialize` method which is assumed to be implicitly called before the adversary program starts.
+`Initialize` also has the ability to return information to the adversary that they may use during the attack (for example, adversaries should be provided the public key when attacking public key encryption).
+An example of a game file defining CPA security for symmetric encryption schemes is provided below.
+
+```
+import 'examples/Primitives/SymEnc.primitive';
+
+Game Left(SymEnc E) {
+    E.Key k;
+    Void Initialize() {
+        k = E.KeyGen();
+    }
+    E.Ciphertext Eavesdrop(E.Message mL, E.Message mR) {
+        return E.Enc(k, mL);
+    }
+}
+
+Game Right(SymEnc E) {
+    E.Key k;
+    Void Initialize() {
+        k = E.KeyGen();
+    }
+    E.Ciphertext Eavesdrop(E.Message mL, E.Message mR) {
+        return E.Enc(k, mR);
+    }
+}
+
+export as CPA;
+```
+In a proof file, we can then reference these two games by writing `CPA(E).Left` and `CPA(E).Right`.
diff --git a/files/index.md b/files/index.md
@@ -0,0 +1,14 @@
+---
+title: Files
+layout: default
+has_children: true
+has_toc: false
+---
+
+ProofFrog has four types of files: [Primitive Files]({% link files/primitive.md %}), [Scheme Files]({% link files/scheme.md %}), [Game Files]({% link files/game.md %}) and [Proof Files]({% link files/proof.md %}).
+
+Proof files are the only type of file that ProofFrog actually verifies, the remaining exist to provide definitions of security definitions and schemes to be used in proofs.
+
+Examples for the syntax of each file can be found on the [Examples]({% link examples.md %}) page.
+
+The full grammar for each of the file types, in ANTLR 4 syntax, can be found in [the GitHub repo](https://github.com/ProofFrog/ProofFrog/tree/main/proof_frog/antlr)
diff --git a/files/primitive.md b/files/primitive.md
@@ -0,0 +1,27 @@
+---
+title: Primitive Files
+layout: default
+parent: Files
+nav_order: 1
+---
+
+# Primitive Files
+
+One can think of primitives as abstract classes from object oriented programming.
+A primitive file allows a user to describe the sets and functions that are associated with a particular mathematical object.
+A primitive contains constant fields and method signatures.
+An example of a primitive for an abstract symmetric encryption scheme is shown below.
+
+```
+Primitive SymEnc(Set MessageSpace, Set CiphertextSpace, Set KeySpace) {
+    Set Message = MessageSpace;
+    Set Ciphertext = CiphertextSpace;
+    Set Key = KeySpace;
+
+    Key KeyGen();
+    Ciphertext Enc(Key k, Message m);
+    Message Dec(Key k, Ciphertext c);
+}
+```
+
+It is parameterized by three sets, and "stores" these sets as fields to be used in type-checking later on. It also defines method signatures for key generation, encryption, and decryption.
diff --git a/files/proof.md b/files/proof.md
@@ -0,0 +1,57 @@
+---
+title: Proof Files
+layout: default
+parent: Files
+nav_order: 4
+---
+
+# Proof Files
+
+Proof files allow the user to specify any reductions or intermediate games that may be used in the proof, after which the user must define statements in four sections: the `let` section, the `assume` section, the `theorem` section, and a sequence of games.
+The `let` section details the variables, primitives, and schemes to be used in the assumptions, theorem, and proof.
+The `assume` section allows the user to specify indistinguishability assumptions for schemes defined in the `let` section.
+The `theorem` section states which security definition is going to be proved for which scheme.
+Finally, the `games` section lists a sequence of games, starting with one of the games from the pair specified in the theorem and ending with the other game.
+Each game in the sequence is checked to be either interchangeable with the next game, or to be indistinguishable with the next game.
+Indistinguishability only occurs if the author writes a reduction to utilize a previously specified indistinguishability assumption.
+An example proof file is shown below, which ProofFrog can verify to show that CPA$ security for a symmetric encryption scheme implies CPA security.
+
+```
+import 'examples/Primitives/SymEnc.primitive';
+import 'examples/Games/SymEnc/CPA.game';
+import 'examples/Games/SymEnc/CPA$.game';
+
+Reduction R1(SymEnc E) compose CPA$(E) against CPA(E).Adversary {
+    E.Ciphertext Eavesdrop(E.Message mL, E.Message mR) {
+        return challenger.CTXT(mL);
+    }
+}
+
+Reduction R2(SymEnc E) compose CPA$(E) against CPA(E).Adversary {
+    E.Ciphertext Eavesdrop(E.Message mL, E.Message mR) {
+        return challenger.CTXT(mR);
+    }
+}
+
+proof:
+
+let:
+    Set MessageSpace;
+    Set CiphertextSpace;
+    Set KeySpace;
+    SymEnc E = SymEnc(MessageSpace, CiphertextSpace, KeySpace);
+
+assume:
+    CPA$(E);
+
+theorem:
+    CPA(E);
+
+games:
+    CPA(E).Left against CPA(E).Adversary;
+    CPA$(E).Real compose R1(E) against CPA(E).Adversary;
+    CPA$(E).Random compose R1(E) against CPA(E).Adversary;
+    CPA$(E).Random compose R2(E) against CPA(E).Adversary;
+    CPA$(E).Real compose R2(E) against CPA(E).Adversary;
+    CPA(E).Right against CPA(E).Adversary;
+```
diff --git a/files/scheme.md b/files/scheme.md
@@ -0,0 +1,47 @@
+---
+title: Scheme Files
+layout: default
+parent: Files
+nav_order: 2
+---
+
+# Scheme Files
+
+One can think of schemes as concrete classes from object oriented programming.
+Each scheme file provides one scheme which "extends" from a primitive.
+A scheme must define the same fields as the primitive it extends, and provide definitions for each primitive method signature.
+An example of a scheme for a symmetric encryption scheme composed from two other symmeteric encryption schemes is shown below.
+
+```
+import 'examples/Primitives/SymEnc.primitive';
+
+Scheme DoubleSymEnc(SymEnc S, SymEnc T) extends SymEnc {
+    requires S.Ciphertext == T.Message;
+
+    Set Message = S.Message;
+    Set Ciphertext = T.Ciphertext;
+    Set Key = S.Key * T.Key;
+
+    Key KeyGen() {
+        S.Key key1 = S.KeyGen();
+        T.Key key2 = T.KeyGen();
+        return [key1, key2];
+    }
+
+    Ciphertext Enc(Key k, Message m) {
+        S.Ciphertext c1 = S.Enc(k[0], m);
+        T.Ciphertext c2 = T.Enc(k[1], c1);
+        return c2;
+    }
+
+    Message Dec(Ciphertext c) {
+    	S.Ciphertext c2 = T.Dec(k[1], c);
+    	S.Message m = S.Dec(k[0], c2);
+    	return m;
+    }
+}
+```
+
+The SymEnc primitive is referenced via the import statement.
+Schemes may also use a `requires` syntax to place bounds on the parameterization via some boolean expression.
+We can see that we define the fields as appropriate for this scheme and also define method definitions for `KeyGen`, `Enc`, and `Dec` that just compose the previous two method definitions.
diff --git a/functionality.md b/functionality.md
@@ -0,0 +1,28 @@
+---
+title: Engine Functionality
+layout: default
+---
+
+# Engine Functionality
+
+A diagram for Proof Frog's engine functionality in full is presented below.
+
+![ProofFrog Functionality Diagram](/assets/diagram.png)
+
+- The `InstantiationTransformer` takes parameterized ASTs and rewrites parameters in terms of variables defined inside the `let` section of the proof file.
+- The `InlineTransformer` is used to inline function calls. This can happen during composition of games with reductions, or when calling a scheme method from within a game's oracle.
+- "Tuple Expansion" takes tuples where the indices for all reads and writes can be statically determined, and rewrites them as multiple variable declarations.
+- ["Copy Propagation](https://en.wikipedia.org/wiki/Copy_propagation)" removes variables that are copies of others
+- "Statement Sorting" attempts to create a canonical ordering of statements within a block via a combination of depth first search and topological sorting. It also performs dead code elimination for statements that have no effect on the return value of an oracle.
+- "Slice Simplification" is an advanced form of copy propagation used when one variable is a copy of another, but there is an intermediate concatenated bitstring that the variable is sliced out of
+- "Symbolic Computation" takes integer variables and simplifies expressions they are used in into a simplest form via [SymPy](https://www.sympy.org/en/index.html)
+- The "Remove Duplicated Fields" transformation searches each pair of fields in a game with the same type and unifies the values if it can be statically determined they share the same value throughout the game's entire lifetime
+- The "Apply User Assumptions" transformation utilizes assumptions about variables that a user can specify between pair of games to simplify conditions
+- "Apply Branch Elimination" takes branches where the conditions are `true` or `false` and simplifies them
+- "Remove Unnecessary Fields" deletes any fields that do not effect the return value of any oracle
+- "Canonicalize Returns" takes return statements that return variables and (when the value of the variable can be statically determined) rewrite them to return that variable
+- "Collapse Branches" takes adjacent if/else-if branches with identical blocks of code and rewrites them into one branch where the condition is the OR of the previous two conditions
+- "Simplify Not Operations" just takes `!(a == b)` and rewrites it to `a != b`
+- "Simplify Tuple Copies" takes tuples of the form `[a[0], a[1], ..., a[n-1]]` and rewrites them into just `a`
+- "Remove Unreachable Code" attempts to use [Z3](https://github.com/Z3Prover/z3) to determine when a return statement is guaranteed to have executed, and deletes all code remaining in an oracle past that point
+- Normalization of field and variable names just assigns each field a numeric name based on the first appearance in the AST.
diff --git a/index.md b/index.md
@@ -1,19 +1,20 @@
 ---
 title: Proof Frog
 layout: home
+nav_order: 1
 ---
 
-ProofFrog is a tool for verifying game-hopping proofs.
+ProofFrog is a work-in-progress tool for verifying cryptographic game-hopping proofs. All security properties in ProofFrog are written via pairs of indistinguishable games.
 
 # Installation
 
-ProofFrog is implemented in python and can be installed using `pip`:
+ProofFrog is implemented in Python and can be installed using `pip`:
 
 `pip install proof_frog`
 
 The `proof_frog` CLI will then be available on your PATH.
 
-Examples of proof_frog files can be found in the [examples git repository](https://github.com/ProofFrog/examples).
+A list of examples is given in [Examples]({% link examples.md %}) page.
 
 For example:
 
diff --git a/philosophy.md b/philosophy.md
@@ -0,0 +1,15 @@
+---
+title: Design Philosophy
+layout: default
+---
+
+# Design Philosophy
+
+ProofFrog takes a novel approach in that it focuses purely on high-level manipulations of games as abstract syntax trees (ASTs) instead of working at the level of logical formulae.
+Treating games as ASTs allows us to leverage techniques from compiler design
+and static analysis to prove output equivalence of games; thereby allowing us to demonstrate the validity of hops in a game sequence.
+The main technique used in our engine is to take pairs of game ASTs and perform a variety of transformations in an attempt to coerce each AST into a canonical form.
+If each pair of ASTs in a game hop can be made equivalent, then our proof engine can assert the validity of the hop.
+ProofFrog also targets ease of use: although it implements a domain-specific language that a user must learn, the language has an imperative C-like syntax that should be comfortable for the average cryptographer.
+Furthermore, it performs transformations to the ASTs with little user guidance which makes writing a proof in many cases as simple as just specifying the hops.
+Finally, the proof syntax attempts to mimic closely to that of a typical pen-and-paper proof.
diff --git a/prooffrog.png b/prooffrog.png

Original file line number	Diff line number	Diff line change
`@@ -0,0 +1 @@`
	`1`	`+<link rel="stylesheet" href="https://cdn.jsdelivr.net/npm/katex@0.11.1/dist/katex.min.css" integrity="sha384-zB1R0rpPzHqg7Kpt0Aljp8JPLqbXI3bhnPWROx27a9N0Ll6ZP/+DiW/UqRcLbRjq" crossorigin="anonymous">`