Attention une mise à jour du service Gitlab va être effectuée le mardi 18 janvier (et non lundi 17 comme annoncé précédemment) entre 18h00 et 18h30. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes.

  1. 07 Jan, 2022 1 commit
    • BLANCHET Bruno's avatar
      TLS 1.3 examples using PRF-ODH + Improved modelling of Diffie-Hellman · bd0ab15c
      BLANCHET Bruno authored
      Merge of branch 2021.24.tls_prfodh
      
      - Added TLS 1.3 examples using PRF-ODH
      - Improved modelling of Diffie-Hellman in the standard library of primitives:
         - DH_proba_collision and square_DH_proba_collision no longer include
           DH_basic
         - the last 2 arguments of DH_single_coord_ladder, DH_X25519, DH_X448
           are functions is_zero_G, is_zero_subG instead of constants zero, sub_zero
           (that allows prime order groups to satisfy these properties, with
           is_zero_G(X) always false)
         - new macros DH_subgroup, DH_exclude_weak_keys, DH_basic_with_is_neutral,
           DH_subgroup_with_is_neutral, is_neutral_DH_proba_collision
         - fixed (square_)PRF_ODH2 so that they can be applied to both
           full Curve25519/448 and subsets generated by g.
      bd0ab15c
  2. 05 Jan, 2022 1 commit
  3. 08 Dec, 2021 1 commit
  4. 30 Nov, 2021 2 commits
  5. 17 Nov, 2021 1 commit
  6. 29 Oct, 2021 1 commit
  7. 01 Oct, 2021 1 commit
  8. 22 Sep, 2021 1 commit
  9. 14 Sep, 2021 1 commit
  10. 08 Sep, 2021 3 commits
  11. 07 Sep, 2021 1 commit
  12. 06 Sep, 2021 1 commit
  13. 15 Aug, 2021 1 commit
  14. 14 Aug, 2021 3 commits
  15. 13 Aug, 2021 2 commits
  16. 28 May, 2021 2 commits
  17. 27 May, 2021 2 commits
    • BLANCHET Bruno's avatar
      updated TODO, .gitignore · b9f15f72
      BLANCHET Bruno authored
      b9f15f72
    • BLANCHET Bruno's avatar
      Fixed several bugs in generation of OCaml implementations · 3423a6fd
      BLANCHET Bruno authored
      Merge of branch 2021.21.order_impl
      
      - the order of evaluation of terms was sometimes incorrect for terms
        that contain insert/get/event_abort
      - let pat = M in yield else p executed p even when the pattern-matching
        succeeded
      - fixed syntax error in the translation of get terms
      - inside events, do not ignore event_abort as well as insert even when it
        appears via a call to a letfun
      3423a6fd
  18. 21 May, 2021 1 commit
  19. 13 May, 2021 1 commit
    • BLANCHET Bruno's avatar
      Fixed several bugs and improved extraction of information from non-simple terms · eab13da5
      BLANCHET Bruno authored
      Merge of branch 2021.20.fix_bug
      
      - fixed bug with negation in extraction of information from non-simple terms
      - fixed internal error when trying to prove unique a find that has conditions containing if/let/find/new/event_abort
      - fixed internal error: else case of LetE was missing in transf_tables
      - fixed bug: do not move event_abort outside a condition of find in expansion
      - improved extraction of information from non-simple terms
      eab13da5
  20. 14 Apr, 2021 1 commit
    • BLANCHET Bruno's avatar
      GDH/square GDH: add PRerandomDist even without RSR + minor changes · 3d4d5b7d
      BLANCHET Bruno authored
      Merge of branch 2021.19.GDH_PDistRerandom
      
      - GDH/square GDH: add PRerandomDist even without RSR
      (because when exponents are chosen according to the spec of
      Curve25519/448, there may be several exponents for the same
      public key, making the DDH oracle ambiguous; I need to choose
      exponents in k[(p+1)/2,p-1] to make sure that the correspondence
      between exponents and public keys is bijective).
      - Mentioned in the manual that when the underlying group is
      curve25519/448, PRF-ODH2 must be applied with the detailed model
      of curve25519/448 (because the existence of equivalent public
      keys breaks the property).
      3d4d5b7d
  21. 07 Apr, 2021 1 commit
  22. 05 Apr, 2021 1 commit
  23. 04 Apr, 2021 2 commits
  24. 03 Apr, 2021 2 commits
    • BLANCHET Bruno's avatar
      2d45a4ae
    • BLANCHET Bruno's avatar
      Reimplemented the counting of calls to oracles in the crypto transformation + minor changes · 2f896c17
      BLANCHET Bruno authored
      Merge of branch 2021.16.fix_proba_bug
      
      Reimplemented the counting of calls to oracles in the crypto
      transformation, to make it more precise and fix two bugs.
      - when computing a replication bound, exploit that we count the number
      of calls or random generations *for each random variable chosen above
      the replication*, hence these random variables must be the same: same
      names, same indices.
      - use defined variables (in addition to known facts) to show that
      two oracle calls are incompatible. For that, compute the incompatibility
      information between program points; that leads to removing some
      useless branches in the output the crypto transformation.
      - in incompatibility tests between oracles, make sure that indices
      are mapped in a coherent way.
      - when trying to eliminate indices, prove that the oracle call is the
      same (instead of proving that all indices are the same) assuming fixed
      counted indices and possibly different uncounted indices. That allows
      to eliminate more counted indices.
      - also apply these elimination of indices and incompatibility tests to
      the counting of creations of random variables.
      - count the creations of random variables, do not try to count how
      many are used in oracles, so count them at their creation point.
      (That's cleaner.)
      - Improvements in detection of subsumed oracle calls
        * Use known facts at oracle2 to perform the matching.
        * Improved matching modulo both the equational theory and known equalities
          from the protocol.
        * Do not redo the filtering of indices when it removed nothing.
        * When several oracle calls are subsumed by the newly added oracle call,
          remove all of them.
      - do not consider as incompatible oracle calls that have probabilities
      #O for different O, even when they are in different branches: these
      probabilities must be added.
      (Bug exhibited in examplesnd/otest/proba_countO_diffbranch2.ocv)
      - fixed bug: when an oracle call O1 was detected as being an instance
      of O2, the compability information for O2 was correctly kept, but
      sometimes the probability for O1 was kept instead of the probability
      for O2.
      (Bug exhibited in examplesnd/otest/bug_same_oracle_call.ocv)
      - optimized the algorithm by using an algorithm for computing the
      maximum independent set in a graph.
      
      - In Diffie-Hellman macros, when there is an oracle ODHa9(x) = exp(g,
      mult(a,x)), add #ODHa9 * time(exp) to the runtime of the context. Same
      for ODHb9.
      - In GDH macros, avoid counting m = exp(g,a) as a call to
      m = exp(m',a) (a call to the DDH oracle), since it can be computed by
      comparing with the public key. Done by adding a specific oracle for
      m = exp(g,a)
      - HPKE: allow eliminating a bit more collisions, to get nicer
      probabilities (DDH queries in O(qH) in the application of GDH)
      - Improved probabilities in OEKE, by a more precise manual guidance.
      2f896c17
  25. 15 Mar, 2021 1 commit
  26. 14 Mar, 2021 1 commit
    • BLANCHET Bruno's avatar
      nicer display of times; fixed confusion between time for the context of a... · d7ba0be1
      BLANCHET Bruno authored
      nicer display of times; fixed confusion between time for the context of a crypto transformation and time of the whole game
      
      Merge of branch 2021.14.fix_proba_bug
      
      - fixed bug: confusion between time for the context of a
      crypto transformation and time of the whole game when
      a collision statement is applied together with the crypto
      transformation
      - nicer display of times (more sharing of formulas)
      - fixed display of inj-event in latex output
      d7ba0be1
  27. 10 Mar, 2021 1 commit
  28. 09 Mar, 2021 1 commit
    • BLANCHET Bruno's avatar
      added construct optim-if in probability formulas · 6ecef6c1
      BLANCHET Bruno authored
      Merge of branch 2021.12.proba_optim_if
      
      - added construct optim-if in probability formulas.
      - use it to optimize the computation of the runtime of the context
      when adding a replication on top of an equiv declaration.
      6ecef6c1
  29. 05 Mar, 2021 1 commit
    • BLANCHET Bruno's avatar
      allow p^n in probabilities + minor changes · 59c7d945
      BLANCHET Bruno authored
      Merge of branch 2021.11.proba_power
      
      - allow p^n in probabilities
      - check for overflows in the computations of exponents of polynoms
      - share common part of probaf between the 2 front-ends in the parser
      - textsecure uses square GDH, name the probability accordingly
      59c7d945
  30. 02 Mar, 2021 1 commit