Commits

Branch selector

 1.0

User selector

bgregoir

Datepicker

All time

Commit History

Commits on Jul 24, 2018

• fix condition in the rule for asynchrone while

  bgregoir

  committed
  d3a650a

Commits on Jul 12, 2018

• fix the checking of generated name in TheoryReplay

  bgregoir

  committed
  71f975a

Commits on Jul 10, 2018

• fix error in"unroll for" tactic in case of hoare and phoare

  bgregoir

  committed
  97e5b1d

Commits on Jun 21, 2018

• add nix

  bgregoir

  committed
  e50b7a7

Commits on Jun 12, 2018

• New tactic for static unrolling of "for-loops"

  Show description for ba545a9
  

  bgregoir

  authored and

  strub

  committed
  ba545a9

Commits on Apr 26, 2018

• improve "include" in module type and module.

  Show description for 64c24ed
  bgregoir

  committed
  64c24ed

• Module type include & bulk proc aliasing

  Show description for 7f33e2a
  

  bgregoir

  authored and

  strub

  committed
  7f33e2a

Commits on Apr 24, 2018

• prove the equivalence between two versions of CPA LR and b.

  bgregoir

  committed
  728c306

Commits on Apr 20, 2018

• fix [#17369] : bug in printing of module application

  bgregoir

  committed
  526d0c0

Commits on Dec 18, 2017

• more ways to do the proof

  bgregoir

  committed
  19c5eed

Commits on Dec 14, 2017

• Add alternative proof in PIR.

  bgregoir

  committed
  ddc2701

• more lemmas on FSet.oflist

  bgregoir

  committed
  fe76f33

Commits on Dec 8, 2017

• add new example: Private information retrieval.

  bgregoir

  committed
  527d9ad

Commits on Jul 28, 2017

• remove garbage

  bgregoir

  committed
  68f7b62

• full proof of cramer shoup :-)

  bgregoir

  committed
  d5c7c6e

• new theory allowing to switch from a sampling d to a sampling d \ X

  bgregoir

  committed
  00a61be

• more lemmas

  bgregoir

  committed
  cbeb6f3

• fix bug in typing of projection on tuple.

  Show description for 55cc1ec
  bgregoir

  committed
  55cc1ec

• intermediary stuff

  bgregoir

  committed
  00cc7d0

Commits on Jul 24, 2017

• bound the probability that an adversary distinguish between the oracle x <@ d \ X and x <@ d

  bgregoir

  committed
  b4c2a37

• more info when local lemma fail.

  bgregoir

  committed
  e401883

Commits on Jul 21, 2017

• fix some theories

  bgregoir

  committed
  e456402

• restart the proof of cramershoup

  bgregoir

  committed
  3e10ebb

• more lemma on distribution

  bgregoir

  committed
  d831de8

• Fix error in the definition of PKE (cstar was not initialised)

  bgregoir

  committed
  7dccbf0

• add the ceil and floor functions

  bgregoir

  committed
  78c7d52

• fix bug in bypr and put some condition in the good order.

  bgregoir

  committed
  ebadb1b

Commits on Mar 24, 2017

• Use “is_lossless” and "predT" in rnd rules

  Show description for 1079832
  bgregoir

  committed
  1079832

Commits on Mar 22, 2017

• add the “selected” option to smt tactic

  Show description for 4950e67
  bgregoir

  committed
  4950e67

Commits on Mar 20, 2017

• Switching EasyCrypt && stdlib to new distributions library

  bgregoir

  committed
  17ab666

Commits on Mar 19, 2017

• add surjective predicate

  

  bgregoir

  authored and

  strub

  committed
  91de244

• add lemma on big and <

  

  bgregoir

  authored and

  strub

  committed
  54d6905

Commits on Mar 18, 2017

• Fix ROM example

  bgregoir

  committed
  5b99fff

Commits on Mar 17, 2017

• Fix printing of random assignment

  bgregoir

  committed
  2a46a2e

Commits on Dec 13, 2016

• add ring on boolean in StdRing.

  bgregoir

  committed
  8acf8d0

Pagination

PreviousNext