hjugement-web/src/Voting/Protocol/Cryptography.purs

   1 module Voting.Protocol.Cryptography where
   2
   3 import Control.Applicative (pure, (<*>))
   4 import Control.Monad (bind)
   5 import Data.Argonaut.Core as JSON
   6 import Data.Argonaut.Decode (class DecodeJson, decodeJson, (.:))
   7 import Data.Argonaut.Encode (class EncodeJson, encodeJson, (:=), (:=?), (~>), (~>?))
   8 import Data.Argonaut.Parser as JSON
   9 import Data.BigInt (BigInt)
  10 import Data.BigInt as BigInt
  11 import Data.Boolean (otherwise)
  12 import Data.Bounded (class Bounded, top)
  13 import Data.Either (Either(..))
  14 import Data.Eq (class Eq, (==), (/=))
  15 import Data.EuclideanRing (class EuclideanRing, (/), mod)
  16 import Data.Foldable (intercalate)
  17 import Data.Function (($), identity, (<<<), flip)
  18 import Data.Functor (class Functor, (<$>))
  19 import Data.HeytingAlgebra ((&&))
  20 import Data.List (List, (:))
  21 import Data.List.Lazy as LL
  22 import Data.Maybe (Maybe(..), maybe, fromJust)
  23 import Data.Monoid (class Monoid, mempty, (<>))
  24 import Data.Newtype (class Newtype, wrap, unwrap)
  25 import Data.Ord (class Ord, (>=))
  26 import Data.Reflection (class Reifies, reflect)
  27 import Data.Ring (class Ring, (-), negate)
  28 import Data.Semiring (class Semiring, zero, (+), one, (*))
  29 import Data.Show (class Show, show)
  30 import Data.String.CodeUnits as String
  31 import Data.Tuple (Tuple(..))
  32 import Effect (Effect)
  33 import Effect.Random (randomInt)
  34 import Node.Crypto as Crypto
  35 import Node.Crypto.Hash as Crypto
  36 import Partial.Unsafe (unsafePartial)
  37 import Type.Proxy (Proxy(..))
  38
  39 import Voting.Protocol.Arithmetic
  40 import Voting.Protocol.Version
  41
  42 -- * Type 'PublicKey'
  43 type PublicKey = G
  44 -- * Type 'SecretKey'
  45 type SecretKey = E
  46
  47 -- * Type 'Hash'
  48 newtype Hash crypto c = Hash (E crypto c)
  49 derive newtype instance eqHash   :: Eq   (Hash crypto c)
  50 derive newtype instance ordHash  :: Ord  (Hash crypto c)
  51 derive newtype instance showHash :: Show (Hash crypto c)
  52
  53 {-
  54 -- | @('hash' bs gs)@ returns as a number in 'G'
  55 -- the 'Crypto.SHA256' hash of the given 'BS.ByteString' 'bs'
  56 -- prefixing the decimal representation of given subgroup elements 'gs',
  57 -- with a comma (",") intercalated between them.
  58 --
  59 -- NOTE: to avoid any collision when the 'hash' function is used in different contexts,
  60 -- a message 'gs' is actually prefixed by a 'bs' indicating the context.
  61 --
  62 -- Used by 'proveEncryption' and 'verifyEncryption',
  63 -- where the 'bs' usually contains the 'statement' to be proven,
  64 -- and the 'gs' contains the 'commitments'.
  65 -}
  66 hash ::
  67  forall crypto c.
  68  CryptoParams crypto c =>
  69  String -> List (G crypto c) ->
  70  Effect (E crypto c)
  71 hash bs gs = do
  72   let s = bs <> intercalate "," (bytesNat <$> gs)
  73   h <- Crypto.hex Crypto.SHA256 s
  74   pure $ fromNatural $ Natural $
  75     unsafePartial $ fromJust $
  76     BigInt.fromBase 16 h
  77
  78 -- | `('bytesNat' x)` returns the serialization of `x`.
  79 bytesNat :: forall n. ToNatural n => n -> String
  80 bytesNat = show <<< nat
  81
  82 -- | `'randomBigInt' low high` returns a random 'BigInt' within `low` and `high`.
  83 --
  84 -- NOTE: adapted from GHC's 'randomIvalInteger'
  85 randomBigInt :: BigInt -> BigInt -> Effect BigInt
  86 randomBigInt l h = do
  87   v <- f one zero
  88   pure (l + v `mod` k)
  89   where
  90   srcLow  = one :: Int
  91   srcHigh = top :: Int
  92   -- | source interval
  93   b = BigInt.fromInt srcHigh - BigInt.fromInt srcLow + one
  94   -- | target interval
  95   k = h - l + one
  96   -- Probabilities of the most likely and least likely result
  97   -- will differ at most by a factor of (1 +- 1/q).
  98   -- Assuming the 'random' is uniform, of course.
  99   -- On average, log q / log b more random values will be generated
 100   -- than the minimum.
 101   q = BigInt.fromInt 1000
 102   targetMagnitude = k * q
 103   -- Generate random values until we exceed the target magnitude.
 104   f mag acc
 105    | mag >= targetMagnitude = pure acc
 106    | otherwise = do
 107      r <- randomInt srcLow srcHigh
 108      f (mag * b)
 109        (acc * b + (BigInt.fromInt r - BigInt.fromInt srcLow))
 110
 111 randomE ::
 112  forall crypto c.
 113  CryptoParams crypto c =>
 114  Effect (E crypto c)
 115 randomE = E <<< Natural <$> randomBigInt zero (unwrap (nat (top::E crypto c)))
 116
 117 -- * Type 'Encryption'
 118 -- | ElGamal-like encryption.
 119 -- Its security relies on the /Discrete Logarithm problem/.
 120 --
 121 -- Because ('groupGen' '^'encNonce '^'secKey '==' 'groupGen' '^'secKey '^'encNonce),
 122 -- knowing @secKey@, one can divide 'encryption_vault' by @('encryption_nonce' '^'secKey)@
 123 -- to decipher @('groupGen' '^'clear)@, then the @clear@ text must be small to be decryptable,
 124 -- because it is encrypted as a power of 'groupGen' (hence the "-like" in "ElGamal-like")
 125 -- to enable the additive homomorphism.
 126 --
 127 -- NOTE: Since @('encryption_vault' '*' 'encryption_nonce' '==' 'encryption_nonce' '^' (secKey '+' clear))@,
 128 -- then: @(logBase 'encryption_nonce' ('encryption_vault' '*' 'encryption_nonce') '==' secKey '+' clear)@.
 129 data Encryption crypto v c = Encryption
 130  { encryption_nonce :: G crypto c
 131    -- ^ Public part of the randomness 'encNonce' used to 'encrypt' the 'clear' text,
 132    -- equal to @('groupGen' '^'encNonce)@
 133  , encryption_vault :: G crypto c
 134    -- ^ Encrypted 'clear' text,
 135    -- equal to @('pubKey' '^'encNone '*' 'groupGen' '^'clear)@
 136  }
 137 derive instance eqEncryption :: Eq (G crypto c) => Eq (Encryption crypto v c)
 138 instance showEncryption :: Show (G crypto c) => Show (Encryption crypto v c) where
 139   show (Encryption e) = show e
 140 instance encodeJsonEncryption ::
 141  ( Reifies v Version
 142  , CryptoParams crypto c
 143  ) => EncodeJson (Encryption crypto v c) where
 144   encodeJson (Encryption{encryption_nonce, encryption_vault}) =
 145     "alpha" := encryption_nonce ~>
 146     "beta"  := encryption_vault ~>
 147     JSON.jsonEmptyObject
 148 instance decodeJsonEncryption ::
 149  ( Reifies v Version
 150  , CryptoParams crypto c
 151  ) => DecodeJson (Encryption crypto v c) where
 152   decodeJson json = do
 153     obj <- decodeJson json
 154     encryption_nonce <- obj .: "alpha"
 155     encryption_vault <- obj .: "beta"
 156     pure $ Encryption{encryption_nonce, encryption_vault}
 157
 158 -- | Additive homomorphism.
 159 -- Using the fact that: @'groupGen' '^'x '*' 'groupGen' '^'y '==' 'groupGen' '^'(x'+'y)@.
 160 instance additiveEncryption ::
 161  CryptoParams crypto c =>
 162  Additive (Encryption crypto v c) where
 163   gzero = Encryption{encryption_nonce:one, encryption_vault:one}
 164   gadd (Encryption x) (Encryption y) = Encryption
 165    { encryption_nonce: x.encryption_nonce * y.encryption_nonce
 166    , encryption_vault: x.encryption_vault * y.encryption_vault
 167    }
 168
 169 -- *** Type 'EncryptionNonce'
 170 type EncryptionNonce = E
 171
 172 -- | @('encrypt' pubKey clear)@ returns an ElGamal-like 'Encryption'.
 173 --
 174 -- WARNING: the secret encryption nonce (@encNonce@)
 175 -- is returned alongside the 'Encryption'
 176 -- in order to 'prove' the validity of the encrypted 'clear' text in 'proveEncryption',
 177 -- but this secret @encNonce@ MUST be forgotten after that,
 178 -- as it may be used to decipher the 'Encryption'
 179 -- without the 'SecretKey' associated with 'pubKey'.
 180 encrypt ::
 181  forall crypto v c.
 182  Reifies v Version =>
 183  CryptoParams crypto c =>
 184  PublicKey crypto c -> E crypto c ->
 185  Effect (Tuple (EncryptionNonce crypto c) (Encryption crypto v c))
 186 encrypt pubKey clear = do
 187   encNonce <- randomE
 188   -- NOTE: preserve the 'encNonce' for 'prove' in 'proveEncryption'.
 189   pure $ Tuple encNonce $
 190     Encryption
 191      { encryption_nonce: groupGen^encNonce
 192      , encryption_vault: pubKey  ^encNonce * groupGen^clear
 193      }
 194
 195 -- * Type 'Proof'
 196 -- | Non-Interactive Zero-Knowledge 'Proof'
 197 -- of knowledge of a discrete logarithm:
 198 -- @(secret == logBase base (base^secret))@.
 199 data Proof crypto v c = Proof
 200  { proof_challenge :: Challenge crypto c
 201    -- ^ 'Challenge' sent by the verifier to the prover
 202    -- to ensure that the prover really has knowledge
 203    -- of the secret and is not replaying.
 204    -- Actually, 'proof_challenge' is not sent to the prover,
 205    -- but derived from the prover's 'Commitment's and statements
 206    -- with a collision resistant 'hash'.
 207    -- Hence the prover cannot chose the 'proof_challenge' to his/her liking.
 208  , proof_response :: E crypto c
 209    -- ^ A discrete logarithm sent by the prover to the verifier,
 210    -- as a response to 'proof_challenge'.
 211    --
 212    -- If the verifier observes that @('proof_challenge' '==' 'hash' statement [commitment])@, where:
 213    --
 214    -- * @statement@ is a serialization of a tag, @base@ and @basePowSec@,
 215    -- * @commitment '==' 'commit' proof base basePowSec '=='
 216    --   base '^' 'proof_response' '*' basePowSec '^' 'proof_challenge'@,
 217    -- * and @basePowSec '==' base'^'sec@,
 218    --
 219    -- then, with overwhelming probability (due to the 'hash' function),
 220    -- the prover was not able to choose 'proof_challenge'
 221    -- yet was able to compute a 'proof_response' such that
 222    -- (@commitment '==' base '^' 'proof_response' '*' basePowSec '^' 'proof_challenge'@),
 223    -- that is to say: @('proof_response' '==' logBase base 'commitment' '-' sec '*' 'proof_challenge')@,
 224    -- therefore the prover knows 'sec'.
 225    --
 226    -- The prover choses 'commitment' to be a random power of @base@,
 227    -- to ensure that each 'prove' does not reveal any information
 228    -- about its secret.
 229  }
 230 derive instance eqProof :: Eq (Proof crypto v c)
 231 instance showProof :: Show (Proof crypto v c) where
 232   show (Proof e) = show e
 233 instance encodeJsonProof ::
 234  ( Reifies v Version
 235  , CryptoParams crypto c
 236  ) => EncodeJson (Proof crypto v c) where
 237   encodeJson (Proof{proof_challenge, proof_response}) =
 238     "challenge" := proof_challenge ~>
 239     "response"  := proof_response ~>
 240     JSON.jsonEmptyObject
 241 instance decodeJsonProof ::
 242  ( Reifies v Version
 243  , CryptoParams crypto c
 244  ) => DecodeJson (Proof crypto v c) where
 245   decodeJson json = do
 246     obj <- decodeJson json
 247     proof_challenge <- obj .: "challenge"
 248     proof_response  <- obj .: "response"
 249     pure $ Proof{proof_challenge, proof_response}
 250
 251 -- ** Type 'ZKP'
 252 -- | Zero-knowledge proof.
 253 --
 254 -- A protocol is /zero-knowledge/ if the verifier
 255 -- learns nothing from the protocol except that the prover
 256 -- knows the secret.
 257 --
 258 -- DOC: Mihir Bellare and Phillip Rogaway. Random oracles are practical:
 259 --      A paradigm for designing efficient protocols. In ACM-CCS’93, 1993.
 260 newtype ZKP = ZKP String
 261
 262 -- ** Type 'Challenge'
 263 type Challenge = E
 264
 265 -- ** Type 'Oracle'
 266 -- An 'Oracle' returns the 'Challenge' of the 'Commitment's
 267 -- by 'hash'ing them (eventually with other 'Commitment's).
 268 --
 269 -- Used in 'prove' it enables a Fiat-Shamir transformation
 270 -- of an /interactive zero-knowledge/ (IZK) proof
 271 -- into a /non-interactive zero-knowledge/ (NIZK) proof.
 272 -- That is to say that the verifier does not have
 273 -- to send a 'Challenge' to the prover.
 274 -- Indeed, the prover now handles the 'Challenge'
 275 -- which becomes a (collision resistant) 'hash'
 276 -- of the prover's commitments (and statements to be a stronger proof).
 277 type Oracle list crypto c = list (Commitment crypto c) -> Challenge crypto c
 278
 279 -- | @('prove' sec commitmentBases oracle)@
 280 -- returns a 'Proof' that @sec@ is known
 281 -- (by proving the knowledge of its discrete logarithm).
 282 --
 283 -- The 'Oracle' is given 'Commitment's equal to the 'commitmentBases'
 284 -- raised to the power of the secret nonce of the 'Proof',
 285 -- as those are the 'Commitment's that the verifier will obtain
 286 -- when composing the 'proof_challenge' and 'proof_response' together
 287 -- (with 'commit').
 288 --
 289 -- WARNING: for 'prove' to be a so-called /strong Fiat-Shamir transformation/ (not a weak):
 290 -- the statement must be included in the 'hash' (along with the commitments).
 291 --
 292 -- NOTE: a 'random' @nonce@ is used to ensure each 'prove'
 293 -- does not reveal any information regarding the secret @sec@,
 294 -- because two 'Proof's using the same 'Commitment'
 295 -- can be used to deduce @sec@ (using the special-soundness).
 296 prove ::
 297  forall crypto v c list.
 298  Reifies v Version =>
 299  CryptoParams crypto c =>
 300  Functor list =>
 301  E crypto c ->
 302  list (G crypto c) ->
 303  Oracle list crypto c ->
 304  Effect (Proof crypto v c)
 305 prove sec commitmentBases oracle = do
 306   nonce <- randomE
 307   let commitments = (_ ^ nonce) <$> commitmentBases
 308   let proof_challenge = oracle commitments
 309   pure $ Proof
 310    { proof_challenge
 311    , proof_response: nonce `op` (sec*proof_challenge)
 312    }
 313   where
 314   -- | See comments in 'commit'.
 315   op =
 316     if reflect (Proxy::Proxy v) `hasVersionTag` versionTagQuicker
 317     then (-)
 318     else (+)
 319
 320 -- | Like 'prove' but quicker. It chould replace 'prove' entirely
 321 -- when Helios-C specifications will be fixed.
 322 proveQuicker ::
 323  forall crypto v c list.
 324  Reifies v Version =>
 325  CryptoParams crypto c =>
 326  Functor list =>
 327  E crypto c ->
 328  list (G crypto c) ->
 329  Oracle list crypto c ->
 330  Effect (Proof crypto v c)
 331 proveQuicker sec commitmentBases oracle = do
 332   nonce <- randomE
 333   let commitments = (_ ^ nonce) <$> commitmentBases
 334   let proof_challenge = oracle commitments
 335   pure $ Proof
 336    { proof_challenge
 337    , proof_response: nonce - sec*proof_challenge
 338    }
 339
 340 -- | @('fakeProof')@ returns a 'Proof'
 341 -- whose 'proof_challenge' and 'proof_response' are uniformly chosen at random,
 342 -- instead of @('proof_challenge' '==' 'hash' statement commitments)@
 343 -- and @('proof_response' '==' nonce '+' sec '*' 'proof_challenge')@
 344 -- as a 'Proof' returned by 'prove'.
 345 --
 346 -- Used in 'proveEncryption' to fill the returned 'DisjProof'
 347 -- with fake 'Proof's for all 'Disjunction's but the encrypted one.
 348 fakeProof ::
 349  forall crypto v c.
 350  CryptoParams crypto c =>
 351  Effect (Proof crypto v c)
 352 fakeProof = do
 353   proof_challenge <- randomE
 354   proof_response  <- randomE
 355   pure $ Proof{proof_challenge, proof_response}
 356
 357 -- ** Type 'Commitment'
 358 -- | A commitment from the prover to the verifier.
 359 -- It's a power of 'groupGen' chosen randomly by the prover
 360 -- when making a 'Proof' with 'prove'.
 361 type Commitment = G
 362
 363 -- | @('commit' proof base basePowSec)@ returns a 'Commitment'
 364 -- from the given 'Proof' with the knowledge of the verifier.
 365 commit ::
 366  forall crypto v c.
 367  Reifies v Version =>
 368  CryptoParams crypto c =>
 369  Proof crypto v c ->
 370  G crypto c ->
 371  G crypto c ->
 372  Commitment crypto c
 373 commit (Proof p) base basePowSec =
 374   (base^p.proof_response) `op`
 375   (basePowSec^p.proof_challenge)
 376   where
 377   op =
 378     if reflect (Proxy::Proxy v) `hasVersionTag` versionTagQuicker
 379     then (*)
 380     else (/)
 381   -- TODO: contrary to some textbook presentations,
 382   -- @('*')@ should be used instead of @('/')@ to avoid the performance cost
 383   -- of a modular exponentiation @('^' ('groupOrder' '-' 'one'))@,
 384   -- this is compensated by using @('-')@ instead of @('+')@ in 'prove'.
 385
 386 -- | Like 'commit' but quicker. It chould replace 'commit' entirely
 387 -- when Helios-C specifications will be fixed.
 388 commitQuicker ::
 389  forall crypto v c.
 390  CryptoParams crypto c =>
 391  Proof crypto v c ->
 392  G crypto c ->
 393  G crypto c ->
 394  Commitment crypto c
 395 commitQuicker (Proof p) base basePowSec =
 396   base^p.proof_response *
 397   basePowSec^p.proof_challenge
 398
 399 -- * Type 'Disjunction'
 400 -- | A 'Disjunction' is an 'inverse'd @('groupGen' '^'opinion)@
 401 -- it's used in 'proveEncryption' to generate a 'Proof'
 402 -- that an 'encryption_vault' contains a given @('groupGen' '^'opinion)@,
 403 type Disjunction = G
 404
 405 booleanDisjunctions :: forall crypto c.  CryptoParams crypto c => LL.List (Disjunction crypto c)
 406 booleanDisjunctions = LL.take 2 $ groupGenInverses::LL.List (G crypto c)