You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: manual/language-reference/execution-model.md
+1-1Lines changed: 1 addition & 1 deletion
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -32,7 +32,7 @@ The security model is **left/right indistinguishability**: a scheme is considere
32
32
33
33
## Game execution model
34
34
35
-
One execution of a game `G` with an adversary `A` proceeds in three stages:
35
+
One execution of a game `G` with an adversary `A` proceeds in four stages:
36
36
37
37
1.**Field initialization.** All state fields are set up. Fields declared with an explicit initializer (`Type x = expr;`) are assigned the value of `expr`. Fields declared without an initializer (`Type x;`) are left in an undefined state until the first assignment.
Copy file name to clipboardExpand all lines: manual/tutorial/otp-ots.md
+6-6Lines changed: 6 additions & 6 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -9,7 +9,7 @@ nav_order: 2
9
9
# Tutorial Part 2 — One-time pad has one-time secrecy
10
10
{: .no_toc }
11
11
12
-
In Tutorial Part 1, you ran an existing proof that that the one-time pad has one-time secrecy, broke it on purpose, and fixed it again. Now you will write that proof from scratch — all four files of it. By the end of this tutorial you will have defined a cryptographic primitive, a security game, a concrete scheme, and a game-hopping proof file, and you will have seen each one type-check or prove green as you finish it. We follow [Joy of Cryptography Section 2.5](https://joyofcryptography.com/provsec/#sec.abstract-defs) closely; if you have Rosulek's textbook handy, keep it open. Everything you write here is already in the `examples/joy/` directory, so you can always peek at the finished version if you get stuck.
12
+
In Tutorial Part 1, you ran an existing proof that the one-time pad has one-time secrecy, broke it on purpose, and fixed it again. Now you will write that proof from scratch — all four files of it. By the end of this tutorial you will have defined a cryptographic primitive, a security game, a concrete scheme, and a game-hopping proof file, and you will have seen each one type-check or prove green as you finish it. We follow [Joy of Cryptography Section 2.5](https://joyofcryptography.com/provsec/#sec.abstract-defs) closely; if you have Rosulek's textbook handy, keep it open. Everything you write here is already in the `examples/joy/` directory, so you can always peek at the finished version if you get stuck.
13
13
14
14
{: .important }
15
15
**Activate your virtual environment first.** Before running any `proof_frog` command in a fresh terminal, activate the Python virtual environment you created during [installation]({% link manual/installation.md %}): `source .venv/bin/activate` on macOS/Linux (bash/zsh), `source .venv/bin/activate.fish` on fish, or `.venv\Scripts\Activate.ps1` on Windows PowerShell. Your prompt should show `(.venv)` once it is active.
@@ -76,7 +76,7 @@ Primitives declare **method signatures only** — there are no method bodies her
76
76
Two new language features appear here:
77
77
78
78
-`Message?` — the `?` suffix denotes a **nullable** (optional) type. In a symmetric encryption scheme, the decryption algorithm `Dec` returns either a `Message` or `None`; decryption is allowed to fail if the ciphertext is invalid. If we later create a scheme returning just plain `Message` where the primitive declared `Message?`, we will get a type mismatch that the engine will catch.
79
-
-`deterministic` — this modifier on `Dec` tells the engine that `Dec` is a deterministic algorithm that always returns the same output for the same inputs. In general, algorithms in FrogLang are assumed to be probabilistics, unless explicitly declared to be deterministic. We will come back to why this matters in Step 4 when the proof engine uses it to justify certain algebraic simplifications.
79
+
-`deterministic` — this modifier on `Dec` tells the engine that `Dec` is a deterministic algorithm that always returns the same output for the same inputs. In general, algorithms in FrogLang are assumed to be probabilistic, unless explicitly declared to be deterministic. We will come back to why this matters in Step 4 when the proof engine uses it to justify certain algebraic simplifications.
@@ -569,15 +569,15 @@ Because `k` is sampled uniformly from `BitString<lambda>` and used exactly once
569
569
570
570
### Diving into the canonical forms
571
571
572
-
ProofFrog's engine works by trying to convert a game in to a "canonical form", by renaming variables to have standard names, removing unused statements, sorting the lines into a canonical order, and applying other mathematical and logical transformations. It then compares the canonical forms of the two games that are being checked for interchangeability.
572
+
ProofFrog's engine works by trying to convert a game into a "canonical form", by renaming variables to have standard names, removing unused statements, sorting the lines into a canonical order, and applying other mathematical and logical transformations. It then compares the canonical forms of the two games that are being checked for interchangeability.
573
573
574
574
In the web editor, you can drill down into the canonical forms derived at each step. When you clicked "Run Proof" above, the Game Hop panel in the bottom left should have been updated to have one line highlighted in green: `OneTimeSecrecy(E).Random ✅`. Click on this green line, and you will see four different chunks of source code appear:
575
575
576
576
{: .lightbox }
577
577
578
578
- Top left: The previous game (`OneTimeSecrecy(E).Real`), with the code of the one-time pad scheme `E` inlined. Notice that the variables from the OTP scheme have a prefix to avoid any collisions between variable names when inserted.
579
579
- Middle left: The current game (`OneTimeSecrecy(E).Random`), with the code of the one-time pad scheme `E` inlined.
580
-
- Top right: The canonicalized form of the previous game, `OneTimeSecrecy(E).Real`. Notice that the variable names have been replaced with canonical versions (`v1`) and that the engine has simplified the program by applyinh a mathematical identity it knows: that the XOR of a uniform random bit string with any bit string is equivalent to just sampling a uniform random bit string.
580
+
- Top right: The canonicalized form of the previous game, `OneTimeSecrecy(E).Real`. Notice that the variable names have been replaced with canonical versions (`v1`) and that the engine has simplified the program by applying a mathematical identity it knows: that the XOR of a uniform random bit string with any bit string is equivalent to just sampling a uniform random bit string.
581
581
- Bottom right: The canonicalized form of the current game, `OneTimeSecrecy(E).Random`. The canonicalization here is more obvious, and no extra transforms were applied.
582
582
583
583
As you can see, the two canonicalized forms are exactly the same: this is why ProofFrog concludes that the hop is valid.
@@ -593,7 +593,7 @@ If you really want to dive into the details of every transformation ProofFrog ap
593
593
594
594
**Proof Failed! Individual hops verified, but the proof is incomplete.** If the first and last game steps use the same side of the theorem (both `Real`, or both `Random`), the engine accepts all individual hops but reports that the overall sequence is incomplete. This is the error you saw in Tutorial Part 1 when you commented out the second game step. Make sure the sequence starts at `Real` and ends at `Random` (or vice versa).
595
595
596
-
**A hop fails.** If the engine cannot verify a hop as an equivalence, it will report which step failed and show a diagnostic. For a proof as small as this one, a failing hop usually means the scheme file has a typo — for example, `k * m` instead of `k + m` in `Enc`. See the [troubleshooting page]({ %link manual/troubleshooting.md %}) for a deeper guide to diagnosing failing steps.
596
+
**A hop fails.** If the engine cannot verify a hop as an equivalence, it will report which step failed and show a diagnostic. For a proof as small as this one, a failing hop usually means the scheme file has a typo — for example, `k * m` instead of `k + m` in `Enc`. See the [troubleshooting page]({% link manual/troubleshooting.md %}) for a deeper guide to diagnosing failing steps.
0 commit comments