0 | module Network.TLS.Signature

  2 | import Data.List

  3 | import Data.Vect

  4 | import Utils.Misc

  5 | import Utils.Bytes

  6 | import Utils.Parser

  7 | import Network.TLS.Parse.PEM

  8 | import Network.TLS.Parse.DER

  9 | import Network.TLS.Parsing

 10 | import Data.String.Parser

 11 | import Crypto.RSA

 12 | import Crypto.Curve

 13 | import Crypto.Curve.Weierstrass

 14 | import Crypto.Hash

 15 | import Crypto.Hash.OID

 17 | public export

 18 | data PublicKey : Type where

 19 |   RsaPublicKey : RSAPublicKey -> PublicKey

 20 |   EcdsaPublicKey : Point p => p -> PublicKey

 22 | public export

 23 | data SignatureParameter : Type where

 24 |   RSA_PKCSv15 : (DPair Type RegisteredHash) -> SignatureParameter

 25 |   RSA_PSS : (wit : DPair Type Hash) -> (salt_len : Nat) -> MaskGenerationFunction -> SignatureParameter

 26 |   ECDSA : DPair Type Hash -> SignatureParameter

 29 | Show PublicKey where

 30 |   show (RsaPublicKey _) = "RSA Public Key"

 31 |   show (EcdsaPublicKey _) = "ECDSA Public Key"

 34 | verify_signature : SignatureParameter -> PublicKey -> List Bits8 -> List Bits8 -> Either String ()

 35 | verify_signature (RSA_PKCSv15 hash_wit) (RsaPublicKey public_key) message signature =

 36 |   if rsassa_pkcs1_v15_verify @{hash_wit.snd} public_key message signature then pure () else Left "signature does not match message"

 37 | verify_signature (RSA_PSS hash_wit salt_len mgf) (RsaPublicKey public_key) message signature =

 38 |   if rsassa_pss_verify' @{hash_wit.snd} mgf salt_len public_key message signature then pure () else Left "signature does not match message"

 39 | verify_signature (ECDSA hash_wit) (EcdsaPublicKey public_key) message signature = do

 40 |   let (Pure [] ok) = feed (map (uncurry MkPosed) $ enumerate Z signature) parse_asn1

 41 |   | (Pure leftover _) => Left "parser overfed for ecdsa signature"

 42 |   | (Fail err) => Left $ "parser error for ecdsa signature: " <+> show err

 43 |   | _ => Left "parser underfed for ecdsa signature"

 44 |   let (Universal ** 16 ** Sequence [ (Universal ** 2 ** IntVal x), (Universal ** 2 ** IntVal y) ] ) = ok

 45 |   | _ => Left "malformed ecdsa signature"

 46 |   let digest = hash @{hash_wit.snd} hash_wit.fst message

 47 |   if ecdsa_verify (be_to_integer digest) (MkSignature public_key (x, y)) then pure () else Left "signature does not match message"

 49 | verify_signature _ _ message signature = Left "public key does not match signature scheme"

 52 | verify_signature' : SignatureParameter -> PublicKey -> List Bits8 -> BitArray -> Either String ()

 53 | verify_signature' param public_key message (MkBitArray 0 signature) = verify_signature param public_key message signature

 54 | verify_signature' param public_key message (MkBitArray n signature) = Left $ "invalid padding: " <+> show n

 57 | extract_algorithm : ASN1Token -> Maybe (List Nat, Maybe ASN1Token)

 58 | extract_algorithm (Universal ** 16 ** Sequence [(Universal ** 6 ** OID algorithm)]) = Just (algorithm, Nothing)

 59 | extract_algorithm (Universal ** 16 ** Sequence ((Universal ** 6 ** OID algorithm) :: parameter :: [])) = Just (algorithm, Just parameter)

 60 | extract_algorithm _ = Nothing

 63 | oid_to_hash_algorithm : List Nat -> Maybe (DPair Type Hash)

 64 | oid_to_hash_algorithm oid =

 65 |   case map natToInteger oid of

 66 |     [ 1, 3, 14, 3, 2, 26 ] => Just (MkDPair Sha1 %search)

 67 |     [ 2, 16, 840, 1, 101, 3, 4, 2, 1 ] => Just (MkDPair Sha256 %search)

 68 |     [ 2, 16, 840, 1, 101, 3, 4, 2, 2 ] => Just (MkDPair Sha384 %search)

 69 |     [ 2, 16, 840, 1, 101, 3, 4, 2, 3 ] => Just (MkDPair Sha512 %search)

 70 |     _ => Nothing

 73 | extract_signature_parameter : List Nat -> Maybe ASN1Token -> Either String SignatureParameter

 74 | extract_signature_parameter oid parameter = do

 75 |   case (map natToInteger oid, parameter) of

 76 |     ([1, 2, 840, 113549, 1, 1, 5], Just (Universal ** 5 ** Null)) =>  Right (RSA_PKCSv15 $ MkDPair Sha1 %search)

 77 |     ([1, 2, 840, 113549, 1, 1, 11], Just (Universal ** 5 ** Null)) => Right (RSA_PKCSv15 $ MkDPair Sha256 %search)

 78 |     ([1, 2, 840, 113549, 1, 1, 12], Just (Universal ** 5 ** Null)) => Right (RSA_PKCSv15 $ MkDPair Sha384 %search)

 79 |     ([1, 2, 840, 113549, 1, 1, 13], Just (Universal ** 5 ** Null)) => Right (RSA_PKCSv15 $ MkDPair Sha512 %search)

 80 |     ([1, 2, 840, 10045, 4, 3, 2], Nothing) => Right (ECDSA $ MkDPair Sha256 %search)

 81 |     ([1, 2, 840, 10045, 4, 3, 3], Nothing) => Right (ECDSA $ MkDPair Sha384 %search)

 82 |     ([1, 2, 840, 10045, 4, 3, 4], Nothing) => Right (ECDSA $ MkDPair Sha512 %search)

 83 |     ([1, 2, 840, 113549, 1, 1, 10], Just (Universal ** 16 ** Sequence params)) => do

 84 |       (wit, params) <- extract_hash_algo params

 85 |       (mgf, params) <- extract_mgf params

 86 |       (salt, params) <- extract_salt_len params

 87 |       extract_trailer params

 88 |       pure $ RSA_PSS wit salt mgf

 89 |     _ => Left "unrecognized signature parameter"

 90 |   where

 91 |     extract_hash_algo' : ASN1Token -> Either String (DPair Type Hash)

 92 |     extract_hash_algo' (Universal ** 16 ** Sequence ((Universal ** 6 ** OID oid) :: _)) =

 93 |       maybe_to_either (oid_to_hash_algorithm oid) "hash algorithm not recognized"

 94 |     extract_hash_algo' _ = Left "malformed hash algorithm"

 96 |     extract_hash_algo : List ASN1Token -> Either String (DPair Type Hash, List ASN1Token)

 97 |     extract_hash_algo [] = Right (MkDPair Sha1 %search, [])

 98 |     extract_hash_algo ((ContextSpecific ** 0 ** UnknownConstructed _ _ [ hash_algo ] ) :: xs) =

 99 |       (, xs) <$> extract_hash_algo' hash_algo

100 |     extract_hash_algo (x :: xs) = Right (MkDPair Sha1 %search, x :: xs)

102 |     extract_mgf : List ASN1Token -> Either String (MaskGenerationFunction, List ASN1Token)

103 |     extract_mgf [] = Right (mgf1 {algo=Sha1}, [])

104 |     extract_mgf ((ContextSpecific ** 1 ** UnknownConstructed _ _ [ sequence ]) :: xs) =

105 |       case sequence of

106 |         ((Universal ** 16 ** Sequence ((Universal ** 6 ** OID oid) :: param :: []))) =>

107 |           case map natToInteger oid of

108 |             [ 1, 2, 840, 113549, 1, 1, 8 ] => (\wit => (mgf1 @{wit.snd}, xs)) <$> extract_hash_algo' param

109 |             _ => Left "mask generation function not recognized"

110 |         _ => Left "malformed mask generation function"

111 |     extract_mgf (x :: xs) = Right (mgf1 {algo=Sha1}, x :: xs)

113 |     extract_salt_len : List ASN1Token -> Either String (Nat, List ASN1Token)

114 |     extract_salt_len [] = Right (20, [])

115 |     extract_salt_len ((ContextSpecific ** 2 ** UnknownConstructed _ _ [ (Universal ** 2 ** IntVal salt_len) ]) :: xs) =

116 |       if salt_len < 0 then Left "negative salt len" else pure (integerToNat salt_len, xs)

117 |     extract_salt_len (x :: xs) = Right (20, x :: xs)

119 |     extract_trailer : List ASN1Token -> Either String ()

120 |     extract_trailer [] = Right ()

121 |     extract_trailer [ (ContextSpecific ** 3 ** UnknownConstructed _ _ [ (Universal ** 2 ** IntVal trailer ) ]) ] =

122 |       if trailer /= 1 then Left "invalid trailer field" else pure ()

123 |     extract_trailer (x :: xs) = Left "unrecognized field after trailer field"

125 | extract_rsa_key : List Bits8 -> Either String RSAPublicKey

126 | extract_rsa_key pk_content = do

127 |   let (Pure [] ok) = feed (map (uncurry MkPosed) $ enumerate Z pk_content) parse_asn1

128 |   | (Pure leftover _) => Left "parser overfed for SubjectPublicKey"

129 |   | (Fail err) => Left $ "parser error for SubjectPublicKey: " <+> show err

130 |   | _ => Left "parser underfed for SubjectPublicKey"

131 |   let (Universal ** 16 ** Sequence

132 |         [ (Universal ** 2 ** IntVal modulus)

133 |         , (Universal ** 2 ** IntVal public_exponent)

134 |         ]

135 |       ) = ok

136 |   | _ => Left "cannot parse SubjectPublicKey"

138 |   maybe_to_either (mk_rsa_publickey modulus public_exponent) "malformed RSA public key"

140 | extract_ecdsa_key : List Bits8 -> List Integer -> Either String PublicKey

141 | extract_ecdsa_key content [1, 2, 840, 10045, 3, 1, 7] =

142 |   EcdsaPublicKey <$> maybe_to_either (decode {p=P256} content) "fail to parse secp256r1 public key"

143 | extract_ecdsa_key content [1, 3, 132, 0, 34] =

144 |   EcdsaPublicKey <$> maybe_to_either (decode {p=P384} content) "fail to parse secp384r1 public key"

145 | extract_ecdsa_key content [1, 3, 132, 0, 35] =

146 |   EcdsaPublicKey <$> maybe_to_either (decode {p=P521} content) "fail to parse secp521r1 public key"

147 | extract_ecdsa_key _ oid = Left $ "unrecognized elliptic curve group oid: " <+> show oid

150 | extract_key' : ASN1Token -> Either String (Vect 20 Bits8, PublicKey)

151 | extract_key' ok = do

152 |   let (Universal ** 16 ** Sequence

153 |         [ algorithm

154 |         , (Universal ** 3 ** Bitstring bitstring)

155 |         ]

156 |       ) = ok

157 |   | _ => Left "cannot parse SubjectPublicKeyInfo"

159 |   let (MkBitArray 0 content) = bitstring

160 |   | _ => Left "incorrect padding for SubjectPublicKey"

162 |   key_info <- maybe_to_either (extract_algorithm algorithm) "cannot parse algorithm in SubjectPublicKeyInfo"

164 |   -- natToInteger is needed because pattern matching list of Nat will kill my cpu big time

165 |   public_key <- case mapFst (map natToInteger) key_info of 

166 |     -- PKCS #1 RSA Encryption

167 |     ([1, 2, 840, 113549, 1, 1, 1], Just (Universal ** 5 ** Null)) =>

168 |       RsaPublicKey <$> extract_rsa_key content

169 |     -- RSA PSS

170 |     ([1, 2, 840, 113549, 1, 1, 10], Nothing) =>

171 |       RsaPublicKey <$> extract_rsa_key content

172 |     -- Elliptic Curve Public Key (RFC 5480)

173 |     ([1, 2, 840, 10045, 2, 1], Just (Universal ** 6 ** OID group_id)) =>

174 |       extract_ecdsa_key content $ map natToInteger group_id

175 |     _ => Left "unrecognized signature algorithm parameter"

177 |   pure (hash Sha1 content, public_key)

180 | extract_key : List Bits8 -> Either String (Vect 20 Bits8, PublicKey)

181 | extract_key der_public_key = do

182 |   let (Pure [] ok) = feed (map (uncurry MkPosed) $ enumerate Z der_public_key) parse_asn1

183 |   | (Pure leftover _) => Left "parser overfed for SubjectPublicKeyInfo"

184 |   | (Fail err) => Left $ "parser error for SubjectPublicKeyInfo: " <+> show err

185 |   | _ => Left "parser underfed for SubjectPublicKeyInfo"

186 |   extract_key' ok