ProofFrog

ProofFrog

ProofFrog

Website Manual Web Editor Guide

File Reference

Language Reference

Reference

Language Reference Tutorial Worked Examples Canonicalization Troubleshooting

Explorer

Game Hops

Open a file from the explorer

ProofFrog

ProofFrog

Select a file from the explorer to start editing.

Website Manual Tutorial Language Reference

Create New Game

Security property name

Parameters

Left side name

Right side name

Create New Primitive

Name

Create New Scheme

Name

Extends primitive

Additional parameters

Create New Proof

Scheme (optional)

Security game

Warning

This proof contains induction steps. The web UI does not currently display induction-related elements correctly.

For full induction support, please use the command-line interface.

Add Import

File to import

Add Primitive Method

Method name

Return type

Parameters

deterministic injective

Add Game Oracle

Target game

Oracle name

Return type

Parameters

Add Assumption

Security property

Arguments

Add Scheme Method

Implement inherited method

Or define a new method

Method name

Return type

Parameters

Add Lemma

Proof file

Theorem (preview)

Arguments

Insert Reduction Hop

Previous game line

Next game line

Assumption

Direction

Reduction

Reduction name

Reduction arguments

New Reduction Stub

Name

Composed security game

Side

Against scheme

Parameters

Compose arguments

New Intermediate Game Stub

Name

Parameters

Inlined Game

Game expression

New File

Folder

File name (without extension)

File type