1. 13 Jul, 2020 2 commits
  2. 25 Jun, 2020 3 commits
  3. 29 May, 2020 1 commit
  4. 09 May, 2020 1 commit
  5. 07 May, 2020 1 commit
  6. 30 Apr, 2020 1 commit
    • Nadim Kobeissi's avatar
      New primitive: blind signatures. · d2261c6b
      Nadim Kobeissi authored
      This commit introduces blind signatures, as requested by Verifpal
      user Professor Marko Schuetz-Schmuck from the University of Puerto
      Two new primitives are introduced: BLIND and UNBLIND. The interface
      works as follows:
      b = BLIND(k, m)
      SIGN(a, b)
      UNBLIND(k, m, SIGN(a, BLIND(k, m))) = SIGN(a, m)
      The purpose of blind signatures is to allow a party to sign a message
      without having access to its contents. To fulfill this purpose, a sender
      "blinds" a message m with "blinding factor" k and sends the resulting
      blinded message m.
      The signer signs the blinded message m with their private key a.
      Then, using UNBLIND and their blinding factor k, the sender can "unblind"
      the signature SIGN(a, BLIND(K, m)) and obtain SIGN(a, m).
      Therfore, the signer signed the message without knowing it, and the
      sender was able to obtain the signature of the signer on the original
      message without revealing the message.
      Note that an attacker possessing b and k can obtain m.
      An example model is included in `examples/blind.vp`.
      Further testing of this new primitive is very much appreciated.
      The Verifpal User Manual and Verifpal for Visual Studio Code will be
      updated momentarily to reflect the new BLIND and UNBLIND primitives.
  7. 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.
  8. 13 Apr, 2020 2 commits
  9. 01 Mar, 2020 1 commit
  10. 29 Feb, 2020 1 commit
    • Nadim Kobeissi's avatar
      Core primitives (with CONCAT and SPLIT) · 87eb7888
      Nadim Kobeissi authored
      Here we introduce the notion of "core primitives", which are simply
      primitives in Verifpal that perform basic operations that are not
      necessarily cryptographic.
      From an engineering perspective as well as from a formal perspective,
      this differentiation is useful because we can allow core primitives
      to have more arbitrarily defined logic than the very rigidly specified
      cryptographic primitives, which have to follow a primitiveSpec struct
      in their specification.
      The three current core primitives are:
      1. ASSERT: used to be a cryptographic primitive, is now a core primitive.
      Works same as before.
      2. CONCAT: Provides concatenation, a very widely requested feature. c =
      CONCAT(a, b). Supports up to five inputs.
      3. SPLIT: Splits concatenated values. a, b = SPLIT(CONCAT(a, b)). Must have
      CONCAT as its input, otherwise Verifpal will return an error and refuse
      to run the analysis.
      CONCAT and SPLIT support is currently experimental and might be buggy. I
      have made some tests of course, but strongly encourage further testing.
      The Verifpal User Manual has been updated to document core primitives.
      The Verifpal syntax highlighting plugins for Visual Studio Code and Vim
      have been updated to support the new CONCAT and SPLIT keywords.
  11. 16 Feb, 2020 2 commits
  12. 15 Feb, 2020 1 commit
  13. 07 Feb, 2020 2 commits
  14. 06 Feb, 2020 1 commit
  15. 05 Feb, 2020 1 commit
  16. 28 Jan, 2020 1 commit
  17. 25 Jan, 2020 1 commit
    • Nadim Kobeissi's avatar
      New feature: modeling passwords/password hashing · 74dc5750
      Nadim Kobeissi authored
      This exciting new feature allows us to declare constants with the
      qualifier "password": like this:
      knows password x
      Now, if x is used as an encryption key or in any other way within a
      primitive, and that primitive is revelaed to the attacker, for example:
      Alice -> Bob: ENC(x, m1), PKE_ENC(G^x, m2)
      The attacker will be able to obtain x and therefore both m1 and m2.
      However, had we done:
      Alice -> Bob: ENC(PW_HASH(x), m1)
      ... then the attacker would not have been able to obtain x or m1. This
      is because values declared with the password qualifier are only usable
      securely in publicly communicated values if first put through a
      primitive that is a password hashing function. The newly introduced
      PW_HASH primitive is currently the only primitive that can act as a
      password hashing function. HASH, HKDF and others won't cut it.
      This is very useful for modeling protocols that include user-provided
      passwords at points, and is a great way to separate guessable passwords
      from material that can actually securely be used as an encryption key of
      some kind.
      I would like to sincerely thank Jean-Philippe Aumasson, who completely
      came up with the idea for this feature. I got so excited about it that I
      implemented it in the same day.
  18. 18 Jan, 2020 1 commit
  19. 10 Jan, 2020 2 commits
  20. 08 Jan, 2020 1 commit
  21. 07 Jan, 2020 2 commits
  22. 06 Jan, 2020 1 commit
  23. 30 Dec, 2019 1 commit
  24. 19 Oct, 2019 1 commit
  25. 15 Sep, 2019 2 commits
  26. 13 Sep, 2019 1 commit
  27. 10 Sep, 2019 1 commit
  28. 09 Sep, 2019 2 commits
  29. 06 Sep, 2019 1 commit
  30. 03 Sep, 2019 1 commit