1. 17 Jan, 2021 2 commits
  2. 05 Jan, 2021 1 commit
  3. 04 Jan, 2021 1 commit
  4. 02 Jan, 2021 3 commits
  5. 01 Jan, 2021 1 commit
  6. 31 Dec, 2020 2 commits
  7. 30 Dec, 2020 2 commits
  8. 05 Dec, 2020 1 commit
  9. 22 Jul, 2020 1 commit
  10. 21 Jul, 2020 2 commits
  11. 19 Jul, 2020 2 commits
  12. 17 Jul, 2020 2 commits
  13. 11 Jul, 2020 2 commits
    • Nadim Kobeissi's avatar
      Remove stack size increase · 52f939f2
      Nadim Kobeissi authored
      52f939f2
    • Nadim Kobeissi's avatar
      Increase maximum stack size · 0a60cd0b
      Nadim Kobeissi authored
      The default Go stack size limit is insufficient for some highly complex
      Verifpal analyses. I have tried to determine whether the stack size was
      being reached due to an infinite loop and evidence suggests that this is
      not the case. Therefore, the stack size limit is increased from the
      default 1GB to 8GB.
      0a60cd0b
  14. 26 Jun, 2020 1 commit
  15. 25 Jun, 2020 4 commits
  16. 24 Jun, 2020 1 commit
  17. 20 May, 2020 1 commit
  18. 10 May, 2020 1 commit
  19. 09 May, 2020 1 commit
  20. 08 May, 2020 1 commit
  21. 07 May, 2020 1 commit
    • Nadim Kobeissi's avatar
      Reorganize project structure into "lib" internals · 36b8e6eb
      Nadim Kobeissi authored
      In order to accomodate the fact that Verifpal will now be translating to
      Coq, ProVerif and soon Go, the project structure inside the `internal`
      folder is now such that we have Verifpal's code itself and a bunch of
      "lib" folders:
      
      - libpeg implements the Verifpal grammar in Peg and generates the
      Verifpal model parser.
      - libcoq implements the Verifpal Coq library/header.
      - libpv implements the Verifpal ProVerif headers.
      - libgo will implement the Verifpal Go implementation headers etc.
      
      Whenever a "lib" is compiled, the resulting artifact goes in
      internal/verifpal/libname.go.
      
      The Makefile should hopefully compile these libs whenever is necessary
      automatically.
      36b8e6eb
  22. 24 Apr, 2020 1 commit
  23. 22 Apr, 2020 1 commit
    • Nadim Kobeissi's avatar
      The Great Exporting · 1be13c9a
      Nadim Kobeissi authored
      Go won't allow struct properties to be marshaled into JSON unless
      they (and their subtypes) are exported.
      
      What a nightmare.
      1be13c9a
  24. 13 Apr, 2020 2 commits
    • Nadim Kobeissi's avatar
      Freshness queries, phases in passive + more · 099c787a
      Nadim Kobeissi authored
      This commit introduces a bunch of things:
      
      - Freshness queries:
          Freshness queries are useful for detecting replay attacks.
          In passive attacker mode, a freshness query will check whether
          a value is "fresh" between sessions (i.e. if it has at least
          one composing element that is generated). In active attacker
          mode, it will check whether a value can be rendered "non-fresh"
          (i.e. static between sessions) and successfully used between
          sessions. This is still an experimental feature.
          Actual documentation will land in the Verifpal User Manual.
      
      - Unlinkability queries:
          Totally not there yet, but this commit introduces them to the
          parser and sanity checker. The query itself does not currently
          do anything.
      
      - Phases:
          Phases now work in passive attacker mode. Previously they only
          worked with an active attacker.
      
      A "freshness.vp" test has been added.
      099c787a
    • Nadim Kobeissi's avatar
      Permissions? · b74e63be
      Nadim Kobeissi authored
      b74e63be
  25. 27 Mar, 2020 1 commit
  26. 26 Mar, 2020 1 commit
  27. 17 Feb, 2020 1 commit