hjugement-protocol/Protocol/Election.hs

   1 {-# LANGUAGE GADTs #-}
   2 {-# LANGUAGE DataKinds #-}
   3 {-# LANGUAGE OverloadedStrings #-}
   4 module Protocol.Election where
   5
   6 import Control.Monad (Monad(..), mapM, forM, join, sequence)
   7 import Data.Bool
   8 import Data.Eq (Eq(..))
   9 import Data.Foldable (Foldable, foldMap, and, toList)
  10 import Data.Function (($), (.))
  11 import Data.Functor (Functor(..), (<$>))
  12 import Data.Int (Int)
  13 import Data.Map.Strict (Map)
  14 import Data.Maybe (Maybe(..), fromJust)
  15 import Data.Monoid (Monoid(..))
  16 import Data.Ord (Ord(..), Ordering(..))
  17 import Data.Proxy (Proxy(..))
  18 import Data.Semigroup (Semigroup(..))
  19 import Data.String (IsString(..))
  20 import Data.Text (Text)
  21 import Data.Tuple (fst, snd, curry)
  22 import GHC.TypeNats
  23 import Numeric.Natural (Natural)
  24 import Prelude (Integral, fromIntegral, undefined, error, min)
  25 import Text.Show (Show(..))
  26 import qualified Control.Monad.Trans.State.Strict as S
  27 import qualified Data.ByteString as BS
  28 import qualified Data.List as List
  29 import qualified Data.Map.Strict as Map
  30 import qualified Data.Text.Encoding as Text
  31
  32 import Protocol.Arithmetic
  33 import Utils.MeasuredList as ML
  34 import qualified Utils.Natural as Nat
  35 import qualified Utils.Constraint as Constraint
  36
  37 -- * Type 'Encryption'
  38 -- | ElGamal-like encryption.
  39 data Encryption q = Encryption
  40  { encryption_nonce :: G q
  41    -- ^ Public part of the random 'secNonce': @('groupGen''^'r)@
  42  , encryption_vault :: G q
  43    -- ^ Encrypted opinion: @('pubKey''^'r '*' 'groupGen''^'opinion)@
  44  } deriving (Eq,Show)
  45
  46 -- | Additive homomorphism.
  47 -- Using the fact that: @'groupGen''^'x '*' 'groupGen''^'y '==' 'groupGen''^'(x'+'y)@.
  48 instance SubGroup q => Additive (Encryption q) where
  49         zero = Encryption one one
  50         x+y = Encryption
  51          (encryption_nonce x * encryption_nonce y)
  52          (encryption_vault x * encryption_vault y)
  53
  54 type PublicKey = G
  55 type SecretKey = E
  56 type SecretNonce = E
  57 type ZKP = BS.ByteString
  58
  59 -- ** Type 'Opinion'
  60 -- | Index of a 'Disjunction' within a 'ML.MeasuredList' of them.
  61 -- It is encoded as an 'E'xponent in 'encrypt'.
  62 type Opinion = Nat.Index
  63
  64 -- | @(encrypt pubKey opinion)@ returns an ElGamal-like 'Encryption'.
  65 --
  66 -- WARNING: the secret nonce is returned alongside the 'Encryption'
  67 -- in order to prove the validity of the encrypted content in 'nizkProof',
  68 -- but this secret nonce MUST be forgotten after that,
  69 -- as it may be used to decipher the 'Encryption'
  70 -- without the secret key associated with 'pubKey'.
  71 encrypt ::
  72  Monad m => RandomGen r => SubGroup q =>
  73  PublicKey q -> Opinion ds ->
  74  S.StateT r m (SecretNonce q, Encryption q)
  75 encrypt pubKey (Nat.Index o) = do
  76         let opinion = inE (natVal o)
  77         secNonce <- random
  78         -- NOTE: preserve the 'secNonce' for 'nizkProof'.
  79         return $ (secNonce,)
  80                 Encryption
  81                  { encryption_nonce = groupGen^secNonce
  82                  , encryption_vault = pubKey  ^secNonce * groupGen^opinion
  83                  -- NOTE: pubKey == groupGen ^ secKey
  84                  -- NOTE: 'opinion' is put as exponent in order
  85                  -- to make an additive homomorphism
  86                  -- instead of a multiplicative homomorphism.
  87                  }
  88
  89 -- * Type 'Signature'
  90 type Signature q = (PublicKey q, Proof q)
  91
  92 -- * Type 'Proof'
  93 data Proof q = Proof
  94  { proof_challenge :: Challenge q
  95  , proof_response  :: E q
  96  } deriving (Eq,Show)
  97
  98 -- ** Type 'Challenge'
  99 type Challenge = E
 100 -- ** Type 'Oracle'
 101 type Oracle q = [Commitment q] -> Challenge q
 102
 103 -- | Fiat-Shamir transformation
 104 -- of an interactive zero-knowledge (IZK) proof
 105 -- into a non-interactive zero-knowledge (NIZK) proof.
 106 nizkProof ::
 107  Monad m => RandomGen r => SubGroup q =>
 108  SecretNonce q -> [Commitment q] -> Oracle q -> S.StateT r m (Proof q)
 109 nizkProof secNonce commits oracle = do
 110         nonce <- random
 111         let commitments = (^ nonce) <$> commits
 112         let proof_challenge = oracle commitments
 113         return Proof
 114          { proof_challenge
 115          , proof_response = nonce + secNonce*proof_challenge
 116          }
 117
 118 -- ** Type 'Commitment'
 119 type Commitment = G
 120
 121 -- ** Type 'Disjunction'
 122 -- | A 'Disjunction' is an 'inv'ersed @'groupGen''^'opinion@
 123 -- it's used in 'proveEncryption' to generate a 'Proof'
 124 -- that an 'encryption_vault' contains a given @'groupGen''^'opinion@,
 125 type Disjunction = G
 126
 127 validBool :: SubGroup q => ML.MeasuredList 2 (Disjunction q)
 128 validBool = fromJust $ ML.fromList $ List.take 2 groupGenInverses
 129
 130 validRange ::
 131  forall q mini maxi proxy.
 132  SubGroup q =>
 133  Bounds mini maxi ->
 134  ML.MeasuredList (maxi-mini) (Disjunction q)
 135 validRange Bounds{}
 136  | Constraint.Proof <- (Nat.<=) @mini @maxi =
 137         fromJust $
 138         ML.fromList $
 139         List.genericTake (Nat.nat @(maxi-mini)) $
 140         List.genericDrop (Nat.nat @mini) $
 141         groupGenInverses
 142
 143 -- ** Type 'ValidityProof'
 144 -- | A list of 'Proof' to prove that the 'Opinion' within an 'Encryption'
 145 -- is indexing a 'Disjunction' within a list of them,
 146 -- without knowing which 'Opinion' it is.
 147 newtype ValidityProof n q = ValidityProof (ML.MeasuredList n (Proof q))
 148  deriving (Eq,Show)
 149
 150 encryptionStatement :: SubGroup q => ZKP -> Encryption q -> BS.ByteString
 151 encryptionStatement zkp Encryption{..} =
 152         "prove|"<>zkp<>"|"<>
 153         fromString (show (intG encryption_nonce))<>","<>
 154         fromString (show (intG encryption_vault))<>"|"
 155
 156 proveEncryption ::
 157  forall ds m r q.
 158  Nat.Known ds =>
 159  Monad m => RandomGen r => SubGroup q =>
 160  PublicKey q -> ZKP ->
 161  ML.MeasuredList ds (Disjunction q) -> Opinion ds ->
 162  (SecretNonce q, Encryption q) ->
 163  S.StateT r m (ValidityProof ds q)
 164 proveEncryption pubKey zkp valids
 165  (Nat.Index (o::Proxy o))
 166  (secNonce, enc@Encryption{..})
 167  -- NOTE: the 'Constraint.Proof's below are needed to prove
 168  -- that the returned 'ValidityProof' has the same length
 169  -- than the given list of 'Disjunction's.
 170  | Constraint.Proof <- (Nat.+<=) @o @1 @ds -- prove that o+1<=ds implies 1<=ds-o and o<=ds
 171  , Constraint.Proof <- (Nat.<=) @o @ds     -- prove that o<=ds implies ds-o is a Natural and o+(ds-o) ~ ds
 172  , Constraint.Proof <- (Nat.<=) @1 @(ds-o) -- prove that ((ds-o)-1)+1 ~ ds-o
 173  = do
 174         let (prevDisjs, _indexedDisj:#nextDisjs) = ML.splitAt o valids
 175         prevFakes <- fakeProof `mapM` prevDisjs
 176         nextFakes <- fakeProof `mapM` nextDisjs
 177         let challengeSum =
 178                 neg $
 179                 sum (proof_challenge . fst <$> prevFakes) +
 180                 sum (proof_challenge . fst <$> nextFakes)
 181         genuineProof <- nizkProof secNonce [groupGen, pubKey] $
 182          -- | 'Oracle'
 183          \nizkCommitments ->
 184                 let commitments =
 185                         foldMap snd prevFakes <>
 186                         nizkCommitments <>
 187                         foldMap snd nextFakes in
 188                 -- NOTE: this is a so-called strong Fiat-Shamir transformation (not a weak):
 189                 -- because the statement is included in the hash (not only the commitments).
 190                 hash (encryptionStatement zkp enc) commitments + challengeSum
 191         return $
 192                 ValidityProof $
 193                         ML.concat
 194                          (fst <$> prevFakes)
 195                          (ML.cons genuineProof (fst <$> nextFakes))
 196         where
 197         fakeProof :: Disjunction q -> S.StateT r m (Proof q, [Commitment q])
 198         fakeProof disj = do
 199                 proof_challenge <- random
 200                 proof_response  <- random
 201                 let commitments =
 202                          [ groupGen^proof_response / encryption_nonce       ^proof_challenge
 203                          , pubKey  ^proof_response / (encryption_vault*disj)^proof_challenge
 204                          ]
 205                 return (Proof{..}, commitments)
 206
 207 validateEncryption ::
 208  SubGroup q =>
 209  PublicKey q -> ZKP ->
 210  ML.MeasuredList n (Disjunction q) ->
 211  (Encryption q, ValidityProof n q) -> Bool
 212 validateEncryption pubKey zkp disjs (enc@Encryption{..}, ValidityProof proofs) =
 213         hash (encryptionStatement zkp enc) commitments == challengeSum
 214         where
 215         challengeSum = sum (proof_challenge <$> proofs)
 216         commitments = foldMap commitment (ML.zip disjs proofs)
 217                 where commitment (disj, Proof{..}) =
 218                         -- g = groupGen
 219                         -- h = pubKey
 220                         -- y1 = encryption_nonce
 221                         -- y2 = (encryption_vault * disj)
 222                         -- com1 = g^res / y1 ^ ch
 223                         -- com2 = h^res / y2 ^ ch
 224                         [ groupGen^proof_response / encryption_nonce       ^proof_challenge
 225                         , pubKey  ^proof_response / (encryption_vault*disj)^proof_challenge
 226                         ]
 227
 228 -- * Type 'Question'
 229 data Question choices (mini::Nat) (maxi::Nat) q =
 230  Question
 231  { question_text    :: Text
 232  , question_answers :: ML.MeasuredList choices Text
 233  , question_bounds  :: Bounds mini maxi
 234  -- , question_blank :: Maybe Bool
 235  } deriving (Eq, Show)
 236
 237 -- ** Type 'Bounds'
 238 data Bounds mini maxi =
 239  ((mini<=maxi), Nat.Known mini, Nat.Known maxi) =>
 240  Bounds (Proxy mini) (Proxy maxi)
 241 instance Show (Bounds mini maxi)
 242 instance Eq (Bounds mini maxi)
 243
 244 -- * Type 'Answer'
 245 data Answer choices mini maxi q = Answer
 246  { answer_opinions :: ML.MeasuredList choices (Encryption q, ValidityProof 2 q)
 247    -- ^ Encrypted 'Opinion' for each 'question_answers'
 248    -- with a 'ValidityProof' that they belong to [0,1].
 249  , answer_sumProof :: ValidityProof (maxi-mini) q
 250    -- ^ Proofs that the sum of the 'Opinon's encrypted in 'answer_opinions'
 251    -- is an element of ['mini'..'maxi'].
 252  -- , answer_blankProof ::
 253  } deriving (Eq,Show)
 254
 255 -- | @(answer pubKey zkp quest opinions)@
 256 -- returns a validable 'Answer',
 257 -- unless the given 'opinions' do not respect 'question_bounds'.
 258 answer ::
 259  forall m r q mini maxi choices.
 260  Monad m => RandomGen r => SubGroup q =>
 261  PublicKey q -> ZKP ->
 262  Question choices mini maxi q ->
 263  ML.MeasuredList choices (Opinion 2) ->
 264  S.StateT r m (Maybe (Answer choices mini maxi q))
 265 answer pubKey zkp Question{..} opinions
 266  | Bounds{} <- question_bounds
 267  , SomeNat (opinionsSum::Proxy opinionsSum) <-
 268    someNatVal $ sum $ (\(Nat.Index o) -> natVal o) <$> opinions
 269    -- prove that opinionsSum-mini is a Natural
 270  , Just Constraint.Proof <- (Nat.<=?) @mini @opinionsSum
 271    -- prove that (opinionsSum-mini)+1 is a Natural
 272  , Constraint.Proof <- (Nat.+) @(opinionsSum-mini) @1
 273    -- prove that maxi-mini is a Natural
 274  , Constraint.Proof <- (Nat.<=) @mini @maxi
 275    -- prove that (opinionsSum-mini)+1 <= maxi-mini
 276  , Just Constraint.Proof <- (Nat.<=?) @((opinionsSum-mini)+1) @(maxi-mini)
 277  = do
 278         encryptions <- encrypt pubKey `mapM` opinions
 279         individualProofs <-
 280                 sequence $ ML.zipWith
 281                  (proveEncryption pubKey zkp validBool)
 282                  opinions encryptions
 283         sumProof <-
 284                 proveEncryption pubKey zkp
 285                  (validRange question_bounds)
 286                  (Nat.Index $ Proxy @(opinionsSum-mini))
 287                  ( sum (fst <$> encryptions)
 288                  , sum (snd <$> encryptions) )
 289         return $ Just Answer
 290          { answer_opinions = ML.zip
 291                  (snd <$> encryptions) -- NOTE: drop secNonce
 292                  individualProofs
 293          , answer_sumProof = sumProof
 294          }
 295  | otherwise = return Nothing
 296
 297 validateAnswer ::
 298  SubGroup q =>
 299  PublicKey q -> ZKP ->
 300  Question choices mini maxi q ->
 301  Answer choices mini maxi q -> Bool
 302 validateAnswer pubKey zkp Question{..} Answer{..} =
 303         and (validateEncryption pubKey zkp validBool <$> answer_opinions) &&
 304         validateEncryption pubKey zkp
 305          (validRange question_bounds)
 306          ( sum (fst <$> answer_opinions)
 307          , answer_sumProof )
 308
 309 -- * Type 'Election'
 310 data Election quests choices mini maxi q = Election
 311  { election_name        :: Text
 312  , election_description :: Text
 313  , election_publicKey   :: PublicKey q
 314  , election_questions   :: ML.MeasuredList quests (Question choices mini maxi q)
 315  , election_uuid        :: UUID
 316  , election_hash        :: Hash
 317  } deriving (Eq,Show)
 318
 319 -- ** Type 'UUID'
 320 newtype UUID = UUID Text
 321  deriving (Eq,Ord,Show)
 322
 323 -- ** Type 'Hash'
 324 newtype Hash = Hash Text
 325  deriving (Eq,Ord,Show)
 326
 327 -- * Type 'Ballot'
 328 data Ballot quests choices mini maxi q = Ballot
 329  { ballot_answers       :: ML.MeasuredList quests (Answer choices mini maxi q)
 330  , ballot_signature     :: Maybe (Signature q)
 331  , ballot_election_uuid :: UUID
 332  , ballot_election_hash :: Text
 333  }