1234567891011121314151617181920212223242526272829303132333435363738394041424344454647484950515253545556575859606162636465666768697071727374757677787980818283848586878889909192939495969798991001011021031041051061071081091101111121131141151161171181191201211221231241251261271281291301311321331341351361371381391401411421431441451461471481491501511521531541551561571581591601611621631641651661671681691701711721731741751761771781791801811821831841851861871881891901911921931941951961971981992002012022032042052062072082092102112122132142152162172182192202212222232242252262272282292302312322332342352362372382392402412422432442452462472482492502512522532542552562572582592602612622632642652662672682692702712722732742752762772782792802812822832842852862872882892902912922932942952962972982993003013023033043053063073083093103113123133143153163173183193203213223233243253263273283293303313323333343353363373383393403413423433443453463473483493503513523533543553563573583593603613623633643653663673683693703713723733743753763773783793803813823833843853863873883893903913923933943953963973983994004014024034044054064074084094104114124134144154164174184194204214224234244254264274284294304314324334344354364374384394404414424434444454464474484494504514524534544554564574584594604614624634644654664674684694704714724734744754764774784794804814824834844854864874884894904914924934944954964974984995005015025035045055065075085095105115125135145155165175185195205215225235245255265275285295305315325335345355365375385395405415425435445455465475485495505515525535545555565575585595605615625635645655665675685695705715725735745755765775785795805815825835845855865875885895905915925935945955965975985996006016026036046056066076086096106116126136146156166176186196206216226236246256266276286296306316326336346356366376386396406416426436446456466476486496506516526536546556566576586596606616626636646656666676686696706716726736746756766776786796806816826836846856866876886896906916926936946956966976986997007017027037047057067077087097107117127137147157167177187197207217227237247257267277287297307317327337347357367377387397407417427437447457467477487497507517527537547557567577587597607617627637647657667677687697707717727737747757767777787797807817827837847857867877887897907917927937947957967977987998008018028038048058068078088098108118128138148158168178188198208218228238248258268278288298308318328338348358368378388398408418428438448458468478488498508518528538548558568578588598608618628638648658668678688698708718728738748758768778788798808818828838848858868878888898908918928938948958968978988999009019029039049059069079089099109119129139149159169179189199209219229239249259269279289299309319329339349359369379389399409419429439449459469479489499509519529539549559569579589599609619629639649659669679689699709719729739749759769779789799809819829839849859869879889899909919929939949959969979989991000100110021003100410051006100710081009101010111012101310141015101610171018101910201021102210231024102510261027102810291030103110321033103410351036103710381039104010411042104310441045104610471048104910501051105210531054105510561057105810591060106110621063106410651066106710681069107010711072107310741075107610771078107910801081108210831084108510861087108810891090typeerror=[|`Invalid_format|`Invalid_length|`Invalid_range|`Not_on_curve|`At_infinity|`Low_order]leterror_to_string=function|`Invalid_format->"invalid format"|`Not_on_curve->"point is not on curve"|`At_infinity->"point is at infinity"|`Invalid_length->"invalid length"|`Invalid_range->"invalid range"|`Low_order->"low order"letpp_errorfmte=Format.fprintffmt"Cannot parse point: %s"(error_to_stringe)letrev_stringbuf=letlen=String.lengthbufinletres=Bytes.createleninfori=0tolen-1doBytes.setres(len-1-i)(String.getbufi)done;Bytes.unsafe_to_stringresexceptionMessage_too_longletbit_atbufi=letbyte_num=i/8inletbit_num=imod8inletbyte=String.get_uint8bufbyte_numinbyteland(1lslbit_num)<>0moduletypeDh=sigtypesecretvalsecret_of_octets:?compress:bool->string->(secret*string,error)resultvalsecret_to_octets:secret->stringvalgen_key:?compress:bool->?g:Mirage_crypto_rng.g->unit->secret*stringvalkey_exchange:secret->string->(string,error)resultendmoduletypeDsa=sigtypeprivtypepubvalbyte_length:intvalbit_length:intvalpriv_of_octets:string->(priv,error)resultvalpriv_to_octets:priv->stringvalpub_of_octets:string->(pub,error)resultvalpub_to_octets:?compress:bool->pub->stringvalpub_of_priv:priv->pubvalgenerate:?g:Mirage_crypto_rng.g->unit->priv*pubvalsign:key:priv->?k:string->string->string*stringvalverify:key:pub->string*string->string->boolmoduleK_gen(H:Digestif.S):sigvalgenerate:key:priv->string->stringendmodulePrecompute:sigvalgenerator_tables:unit->stringarrayarrayarrayendendmoduletypeDh_dsa=sigmoduleDh:DhmoduleDsa:Dsaendtypefield_element=stringtypeout_field_element=bytesmoduletypeParameters=sigvala:field_elementvalb:field_elementvalg_x:field_elementvalg_y:field_elementvalp:field_elementvaln:field_elementvalpident:stringvalbyte_length:intvalbit_length:intvalfe_length:intvalfirst_byte_bits:intoptionendtypepoint={f_x:field_element;f_y:field_element;f_z:field_element}typeout_point={m_f_x:out_field_element;m_f_y:out_field_element;m_f_z:out_field_element}typescalar=ScalarofstringmoduletypeForeign=sigvalmul:out_field_element->field_element->field_element->unitvalsub:out_field_element->field_element->field_element->unitvaladd:out_field_element->field_element->field_element->unitvalto_montgomery:out_field_element->field_element->unitvalfrom_octets:out_field_element->string->unitvalset_one:out_field_element->unitvalnz:field_element->boolvalsqr:out_field_element->field_element->unitvalfrom_montgomery:out_field_element->field_element->unitvalto_octets:bytes->field_element->unitvalinv:out_field_element->field_element->unitvalselect_c:out_field_element->bool->field_element->field_element->unitvaldouble_c:out_point->point->unitvaladd_c:out_point->point->point->unitvalscalar_mult_base_c:out_point->string->unitendmoduletypeField_element=sigvalmul:field_element->field_element->field_elementvalsub:field_element->field_element->field_elementvaladd:field_element->field_element->field_elementvalfrom_montgomery:field_element->field_elementvalzero:field_elementvalone:field_elementvalnz:field_element->boolvalsqr:field_element->field_elementvalinv:field_element->field_elementvalselect:bool->then_:field_element->else_:field_element->field_elementvalfrom_be_octets:string->field_elementvalto_octets:field_element->stringvaldouble_point:point->pointvaladd_point:point->point->pointvalscalar_mult_base_point:scalar->pointendmoduleMake_field_element(P:Parameters)(F:Foreign):Field_element=structletb_utsb=Bytes.unsafe_to_stringbletcreate()=Bytes.createP.fe_lengthletmulab=lettmp=create()inF.multmpab;b_utstmpletsubab=lettmp=create()inF.subtmpab;b_utstmpletaddab=lettmp=create()inF.addtmpab;b_utstmpletfrom_montgomerya=lettmp=create()inF.from_montgomerytmpa;b_utstmpletzero=letb=Bytes.makeP.fe_length'\000'inb_utsbletone=letfe=create()inF.set_onefe;b_utsfeletnza=F.nzaletsqra=lettmp=create()inF.sqrtmpa;b_utstmpletinva=lettmp=create()inF.invtmpa;b_utstmpletselectbit~then_~else_=lettmp=create()inF.select_ctmpbitthen_else_;b_utstmpletfrom_be_octetsbuf=letbuf_rev=rev_stringbufinlettmp=create()inF.from_octetstmpbuf_rev;F.to_montgomerytmp(b_utstmp);b_utstmpletcreate_octets()=Bytes.createP.byte_lengthletto_octetsfe=lettmp=create_octets()inF.to_octetstmpfe;b_utstmpletout_point()={m_f_x=create();m_f_y=create();m_f_z=create();}letout_p_to_pp={f_x=b_utsp.m_f_x;f_y=b_utsp.m_f_y;f_z=b_utsp.m_f_z;}letdouble_pointp=lettmp=out_point()inF.double_ctmpp;out_p_to_ptmpletadd_pointab=lettmp=out_point()inF.add_ctmpab;out_p_to_ptmpletscalar_mult_base_point(Scalard)=lettmp=out_point()inF.scalar_mult_base_ctmpd;out_p_to_ptmpendmoduletypePoint=sigvalat_infinity:unit->pointvalis_infinity:point->boolvaladd:point->point->pointvaldouble:point->pointvalof_octets:string->(point,error)resultvalto_octets:compress:bool->point->stringvalto_affine_raw:point->(field_element*field_element)optionvalx_of_finite_point:point->stringvalparams_g:pointvalselect:bool->then_:point->else_:point->pointvalscalar_mult_base:scalar->pointendmoduleMake_point(P:Parameters)(F:Foreign):Point=structmoduleFe=Make_field_element(P)(F)letat_infinity()=letf_x=Fe.oneinletf_y=Fe.oneinletf_z=Fe.zeroin{f_x;f_y;f_z}letis_infinity(p:point)=not(Fe.nzp.f_z)letis_solution_to_curve_equation=leta=Fe.from_be_octetsP.ainletb=Fe.from_be_octetsP.binfun~x~y->letx3=Fe.mulxxinletx3=Fe.mulx3xinletax=Fe.mulaxinlety2=Fe.mulyyinletsum=Fe.addx3axinletsum=Fe.addsumbinletsum=Fe.subsumy2innot(Fe.nzsum)letcheck_coordinatebuf=(* ensure buf < p: *)matchEqaf.compare_be_with_len~len:P.byte_lengthbufP.p>=0with|true->None|exceptionInvalid_argument_->None|false->Some(Fe.from_be_octetsbuf)(** Convert coordinates to a finite point ensuring:
- x < p
- y < p
- y^2 = ax^3 + ax + b
*)letvalidate_finite_point~x~y=match(check_coordinatex,check_coordinatey)with|Somef_x,Somef_y->ifis_solution_to_curve_equation~x:f_x~y:f_ythenletf_z=Fe.oneinOk{f_x;f_y;f_z}elseError`Not_on_curve|_->Error`Invalid_rangeletto_affine_rawp=ifis_infinitypthenNoneelseletz1=Fe.from_montgomeryp.f_zinletz2=Fe.invz1inletz1=Fe.sqrz2inletz1=Fe.from_montgomeryz1inletx=Fe.mulp.f_xz1inletz1=Fe.mulz1z2inlety=Fe.mulp.f_yz1inSome(x,y)letto_affinep=Option.map(fun(x,y)->Fe.to_octetsx,Fe.to_octetsy)(to_affine_rawp)letto_octets~compressp=letbuf=matchto_affinepwith|None->String.make1'\000'|Some(x,y)->letlen_x=String.lengthxandlen_y=String.lengthyinletres=Bytes.create(1+len_x+len_y)inBytes.setres0'\004';letrev_x=rev_stringxandrev_y=rev_stringyinBytes.unsafe_blit_stringrev_x0res1len_x;Bytes.unsafe_blit_stringrev_y0res(1+len_x)len_y;Bytes.unsafe_to_stringresinifcompressthenletout=Bytes.create(P.byte_length+1)inletident=2+(String.get_uint8buf(P.byte_length*2))land1inBytes.unsafe_blit_stringbuf1out1P.byte_length;Bytes.set_uint8out0ident;Bytes.unsafe_to_stringoutelsebufletdoublep=Fe.double_pointpletaddpq=Fe.add_pointpqletx_of_finite_pointp=matchto_affinepwithNone->assertfalse|Some(x,_)->rev_stringxletparams_g=matchvalidate_finite_point~x:P.g_x~y:P.g_ywith|Okp->p|Error_->assertfalseletselectbit~then_~else_={f_x=Fe.selectbit~then_:then_.f_x~else_:else_.f_x;f_y=Fe.selectbit~then_:then_.f_y~else_:else_.f_y;f_z=Fe.selectbit~then_:then_.f_z~else_:else_.f_z;}letpowxexp=letr0=refFe.oneinletr1=refxinfori=P.byte_length*8-1downto0doletbit=bit_atexpiinletmultiplied=Fe.mul!r0!r1inletr0_sqr=Fe.sqr!r0inletr1_sqr=Fe.sqr!r1inr0:=Fe.selectbit~then_:multiplied~else_:r0_sqr;r1:=Fe.selectbit~then_:r1_sqr~else_:multiplied;done;!r0letdecompress=(* When p = 4*k+3, as is the case of NIST-P256, there is an efficient square
root algorithm to recover the y, as follows:
Given the compact representation of Q as x,
y2 = x^3 + a*x + b
y' = y2^((p+1)/4)
y = min(y',p-y')
Q=(x,y) is the canonical representation of the point
*)letpident=P.pident(* (Params.p + 1) / 4*)inleta=Fe.from_be_octetsP.ainletb=Fe.from_be_octetsP.binletp=Fe.from_be_octetsP.pinfunpk->letx=Fe.from_be_octets(String.subpk1P.byte_length)inletx3=Fe.mulxxinletx3=Fe.mulx3xin(* x3 *)letax=Fe.mulaxin(* ax *)letsum=Fe.addx3axinletsum=Fe.addsumbin(* y^2 *)lety=powsumpidentin(* https://tools.ietf.org/id/draft-jivsov-ecc-compact-00.xml#sqrt point 4.3*)lety'=Fe.subpyinlety=Fe.from_montgomeryyinlety_struct=Fe.to_octetsyin(* number must not be in montgomery domain*)lety_struct=rev_stringy_structinlety'=Fe.from_montgomeryy'inlety_struct2=Fe.to_octetsy'in(* number must not be in montgomery domain*)lety_struct2=rev_stringy_struct2inletident=String.get_uint8pk0inletsignY=2+(String.get_uint8y_struct(P.byte_length-1))land1inletres=ifInt.equalsignYidenttheny_structelsey_struct2inletout=Bytes.create((P.byte_length*2)+1)inBytes.setout0'\004';Bytes.unsafe_blit_stringpk1out1P.byte_length;Bytes.unsafe_blit_stringres0out(P.byte_length+1)P.byte_length;Bytes.unsafe_to_stringoutletof_octetsbuf=letlen=P.byte_lengthinifString.lengthbuf=0thenError`Invalid_formatelseletof_octetsbuf=letx=String.subbuf1leninlety=String.subbuf(1+len)leninvalidate_finite_point~x~yinmatchString.get_uint8buf0with|0x00whenString.lengthbuf=1->Ok(at_infinity())|0x02|0x03whenString.lengthP.pident>0->letdecompressed=decompressbufinof_octetsdecompressed|0x04whenString.lengthbuf=1+len+len->of_octetsbuf|0x00|0x04->Error`Invalid_length|_->Error`Invalid_formatletscalar_mult_base=Fe.scalar_mult_base_pointendmoduletypeScalar=sigvalnot_zero:string->boolvalis_in_range:string->boolvalof_octets:string->(scalar,error)resultvalto_octets:scalar->stringvalscalar_mult:scalar->point->pointvalscalar_mult_base:scalar->pointvalgenerator_tables:unit->field_elementarrayarrayarrayendmoduleMake_scalar(Param:Parameters)(P:Point):Scalar=structletnot_zero=letzero=String.makeParam.byte_length'\000'infunbuf->not(Eqaf.equalbufzero)letis_in_rangebuf=not_zerobuf&&Eqaf.compare_be_with_len~len:Param.byte_lengthParam.nbuf>0letof_octetsbuf=matchis_in_rangebufwith|exceptionInvalid_argument_->Error`Invalid_length|true->Ok(Scalar(rev_stringbuf))|false->Error`Invalid_rangeletto_octets(Scalarbuf)=rev_stringbuf(* Branchless Montgomery ladder method *)letscalar_mult(Scalars)p=letr0=ref(P.at_infinity())inletr1=refpinfori=Param.byte_length*8-1downto0doletbit=bit_atsiinletsum=P.add!r0!r1inletr0_double=P.double!r0inletr1_double=P.double!r1inr0:=P.selectbit~then_:sum~else_:r0_double;r1:=P.selectbit~then_:r1_double~else_:sumdone;!r0(* Specialization of [scalar_mult d p] when [p] is the generator *)letscalar_mult_base=P.scalar_mult_base(* Pre-compute multiples of the generator point
returns the tables along with the number of significant bytes *)letgenerator_tables()=letlen=Param.fe_length*2inletone_table_=Array.init15(fun_->P.at_infinity())inlettable=Array.initlenone_tableinletbase=refP.params_ginfori=0tolen-1dotable.(i).(0)<-!base;forj=1to14dotable.(i).(j)<-P.add!basetable.(i).(j-1)done;base:=P.double!base;base:=P.double!base;base:=P.double!base;base:=P.double!basedone;letconvert{f_x;f_y;f_z}=[|f_x;f_y;f_z|]inArray.map(Array.mapconvert)tableendmoduleMake_dh(Param:Parameters)(P:Point)(S:Scalar):Dh=structletpoint_of_octetsc=matchP.of_octetscwith|Okpwhennot(P.is_infinityp)->Okp|Ok_->Error`At_infinity|Error_ase->eletpoint_to_octets=P.to_octetstypesecret=scalarletshare?(compress=false)private_key=letpublic_key=S.scalar_mult_baseprivate_keyinpoint_to_octets~compresspublic_keyletsecret_of_octets?compresss=matchS.of_octetsswith|Okp->Ok(p,share?compressp)|Error_ase->eletsecret_to_octetss=S.to_octetssletrecgenerate_private_key?g()=letcandidate=Mirage_crypto_rng.generate?gParam.byte_lengthinmatchS.of_octetscandidatewith|Oksecret->secret|Error_->generate_private_key?g()letgen_key?compress?g()=letprivate_key=generate_private_key?g()inprivate_key,share?compressprivate_keyletkey_exchangesecretreceived=matchpoint_of_octetsreceivedwith|Error_aserr->err|Okshared->Ok(P.x_of_finite_point(S.scalar_multsecretshared))endmoduletypeForeign_n=sigvalmul:out_field_element->field_element->field_element->unitvaladd:out_field_element->field_element->field_element->unitvalinv:out_field_element->field_element->unitvalone:out_field_element->unitvalfrom_bytes:out_field_element->string->unitvalto_bytes:bytes->field_element->unitvalfrom_montgomery:out_field_element->field_element->unitvalto_montgomery:out_field_element->field_element->unitendmoduletypeFn=sigvalfrom_be_octets:string->field_elementvalto_be_octets:field_element->stringvalmul:field_element->field_element->field_elementvaladd:field_element->field_element->field_elementvalinv:field_element->field_elementvalone:field_elementvalfrom_montgomery:field_element->field_elementvalto_montgomery:field_element->field_elementendmoduleMake_Fn(P:Parameters)(F:Foreign_n):Fn=structletb_uts=Bytes.unsafe_to_stringletcreate()=Bytes.createP.fe_lengthletcreate_octets()=Bytes.createP.byte_lengthletfrom_be_octetsv=letv'=create()inF.from_bytesv'(rev_stringv);F.to_montgomeryv'(b_utsv');b_utsv'letto_be_octetsv=letbuf=create_octets()inF.to_bytesbufv;rev_string(b_utsbuf)letmulab=lettmp=create()inF.multmpab;b_utstmpletaddab=lettmp=create()inF.addtmpab;b_utstmpletinva=lettmp=create()inF.invtmpa;F.to_montgomerytmp(b_utstmp);b_utstmpletone=lettmp=create()inF.onetmp;b_utstmpletfrom_montgomerya=lettmp=create()inF.from_montgomerytmpa;b_utstmpletto_montgomerya=lettmp=create()inF.to_montgomerytmpa;b_utstmpendmoduleMake_dsa(Param:Parameters)(F:Fn)(P:Point)(S:Scalar)(H:Digestif.S)=structtypepriv=scalarletbyte_length=Param.byte_lengthletbit_length=Param.bit_lengthletpriv_of_octets=S.of_octetsletpriv_to_octets=S.to_octetsletpaddedmsg=letl=String.lengthmsginletbl=Param.byte_lengthinletfirst_byte_ok()=matchParam.first_byte_bitswith|None->true|Somem->(String.get_uint8msg0)land(0xFFland(lnotm))=0inifl>bl||(l=bl&¬(first_byte_ok()))thenraiseMessage_too_longelseifl=blthenmsgelse(letres=Bytes.makebl'\000'inBytes.unsafe_blit_stringmsg0res(bl-l)l;Bytes.unsafe_to_stringres)(* RFC 6979: compute a deterministic k *)moduleK_gen(H:Digestif.S)=structletdrbg:'aMirage_crypto_rng.generator=letmoduleM=Mirage_crypto_rng.Hmac_drbg(H)in(moduleM)letg~keymsg=letg=Mirage_crypto_rng.create~strict:truedrbginMirage_crypto_rng.reseed~g(S.to_octetskey^msg);g(* Defined in RFC 6979 sec 2.3.2 with
- blen = 8 * Param.byte_length
- qlen = Param.bit_length *)letbits2intr=(* keep qlen *leftmost* bits *)letshift=(8*Param.byte_length)-Param.bit_lengthinifshift=0thenBytes.unsafe_to_stringrelse(* Assuming shift is < 8 *)letr'=Bytes.createParam.byte_lengthinletp=ref0x00infori=0toParam.byte_length-1doletx=Bytes.get_uint8riinletv=(xlsrshift)lor(!plsl(8-shift))inp:=x;Bytes.set_uint8r'ivdone;Bytes.unsafe_to_stringr'(* take qbit length, and ensure it is suitable for ECDSA (> 0 & < n) *)letgeng=letrecgo()=letb=Bytes.createParam.byte_lengthinMirage_crypto_rng.generate_into~gbParam.byte_length;(* truncate to the desired number of bits *)letr=bits2intbinifS.is_in_rangerthenrelsego()ingo()letgenerate~keybuf=gen(g~key(paddedbuf))endmoduleK_gen_default=K_gen(H)typepub=pointletpub_of_octets=P.of_octetsletpub_to_octets?(compress=false)pk=P.to_octets~compresspkletgenerate?g()=(* FIPS 186-4 B 4.2 *)letd=letrecone()=matchS.of_octets(Mirage_crypto_rng.generate?gParam.byte_length)with|Okx->x|Error_->one()inone()inletq=S.scalar_mult_basedin(d,q)letx_of_finite_point_mod_np=matchP.to_affine_rawpwith|None->None|Some(x,_)->letx=F.to_montgomeryxinletx=F.mulxF.oneinletx=F.from_montgomeryxinSome(F.to_be_octetsx)letsign~key?kmsg=letmsg=paddedmsginlete=F.from_be_octetsmsginletg=K_gen_default.g~keymsginletrecdo_signg=letagain()=matchkwith|None->do_signg|Some_->invalid_arg"k not suitable"inletk'=matchkwithNone->K_gen_default.geng|Somek->kinletksc=matchS.of_octetsk'with|Okksc->ksc|Error_->invalid_arg"k not in range"(* if no k is provided, this cannot happen since K_gen_*.gen already preserves the Scalar invariants *)inletpoint=S.scalar_mult_basekscinmatchx_of_finite_point_mod_npointwith|None->again()|Somer->letr_mon=F.from_be_octetsrinletkmon=F.from_be_octetsk'inletkinv=F.invkmoninletdmon=F.from_be_octets(S.to_octetskey)inletrd=F.mulr_mondmoninletcmon=F.adderdinletsmon=F.mulkinvcmoninlets=F.from_montgomerysmoninlets=F.to_be_octetssinifS.not_zeros&&S.not_zerorthenr,selseagain()indo_signgletpub_of_privpriv=S.scalar_mult_baseprivletverify~key(r,s)msg=tryletr=paddedrands=paddedsinifnot(S.is_in_ranger&&S.is_in_ranges)thenfalseelseletmsg=paddedmsginletz=F.from_be_octetsmsginlets_mon=F.from_be_octetssinlets_inv=F.invs_moninletu1=F.mulzs_invinletr_mon=F.from_be_octetsrinletu2=F.mulr_mons_invinletu1=F.from_montgomeryu1inletu2=F.from_montgomeryu2inmatchS.of_octets(F.to_be_octetsu1),S.of_octets(F.to_be_octetsu2)with|Oku1,Oku2->letpoint=P.add(S.scalar_mult_baseu1)(S.scalar_multu2key)inbeginmatchx_of_finite_point_mod_npointwith|None->false(* point is infinity *)|Somer'->String.equalrr'end|Error_,_|_,Error_->falsewith|Message_too_long->falsemodulePrecompute=structletgenerator_tables=S.generator_tablesendendmoduleP256:Dh_dsa=structmoduleParams=structleta="\xFF\xFF\xFF\xFF\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFC"letb="\x5A\xC6\x35\xD8\xAA\x3A\x93\xE7\xB3\xEB\xBD\x55\x76\x98\x86\xBC\x65\x1D\x06\xB0\xCC\x53\xB0\xF6\x3B\xCE\x3C\x3E\x27\xD2\x60\x4B"letg_x="\x6B\x17\xD1\xF2\xE1\x2C\x42\x47\xF8\xBC\xE6\xE5\x63\xA4\x40\xF2\x77\x03\x7D\x81\x2D\xEB\x33\xA0\xF4\xA1\x39\x45\xD8\x98\xC2\x96"letg_y="\x4F\xE3\x42\xE2\xFE\x1A\x7F\x9B\x8E\xE7\xEB\x4A\x7C\x0F\x9E\x16\x2B\xCE\x33\x57\x6B\x31\x5E\xCE\xCB\xB6\x40\x68\x37\xBF\x51\xF5"letp="\xFF\xFF\xFF\xFF\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF"letn="\xFF\xFF\xFF\xFF\x00\x00\x00\x00\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xBC\xE6\xFA\xAD\xA7\x17\x9E\x84\xF3\xB9\xCA\xC2\xFC\x63\x25\x51"letpident="\x3F\xFF\xFF\xFF\xC0\x00\x00\x00\x40\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x40\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00"|>rev_string(* (Params.p + 1) / 4*)letbyte_length=32letbit_length=256letfe_length=32letfirst_byte_bits=NoneendmoduleForeign=structexternalmul:out_field_element->field_element->field_element->unit="mc_p256_mul"[@@noalloc]externalsub:out_field_element->field_element->field_element->unit="mc_p256_sub"[@@noalloc]externaladd:out_field_element->field_element->field_element->unit="mc_p256_add"[@@noalloc]externalto_montgomery:out_field_element->field_element->unit="mc_p256_to_montgomery"[@@noalloc]externalfrom_octets:out_field_element->string->unit="mc_p256_from_bytes"[@@noalloc]externalset_one:out_field_element->unit="mc_p256_set_one"[@@noalloc]externalnz:field_element->bool="mc_p256_nz"[@@noalloc]externalsqr:out_field_element->field_element->unit="mc_p256_sqr"[@@noalloc]externalfrom_montgomery:out_field_element->field_element->unit="mc_p256_from_montgomery"[@@noalloc]externalto_octets:bytes->field_element->unit="mc_p256_to_bytes"[@@noalloc]externalinv:out_field_element->field_element->unit="mc_p256_inv"[@@noalloc]externalselect_c:out_field_element->bool->field_element->field_element->unit="mc_p256_select"[@@noalloc]externaldouble_c:out_point->point->unit="mc_p256_point_double"[@@noalloc]externaladd_c:out_point->point->point->unit="mc_p256_point_add"[@@noalloc]externalscalar_mult_base_c:out_point->string->unit="mc_p256_scalar_mult_base"[@@noalloc]endmoduleForeign_n=structexternalmul:out_field_element->field_element->field_element->unit="mc_np256_mul"[@@noalloc]externaladd:out_field_element->field_element->field_element->unit="mc_np256_add"[@@noalloc]externalinv:out_field_element->field_element->unit="mc_np256_inv"[@@noalloc]externalone:out_field_element->unit="mc_np256_one"[@@noalloc]externalfrom_bytes:out_field_element->string->unit="mc_np256_from_bytes"[@@noalloc]externalto_bytes:bytes->field_element->unit="mc_np256_to_bytes"[@@noalloc]externalfrom_montgomery:out_field_element->field_element->unit="mc_np256_from_montgomery"[@@noalloc]externalto_montgomery:out_field_element->field_element->unit="mc_np256_to_montgomery"[@@noalloc]endmoduleP=Make_point(Params)(Foreign)moduleS=Make_scalar(Params)(P)moduleDh=Make_dh(Params)(P)(S)moduleFn=Make_Fn(Params)(Foreign_n)moduleDsa=Make_dsa(Params)(Fn)(P)(S)(Digestif.SHA256)endmoduleP384:Dh_dsa=structmoduleParams=structleta="\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFE\xFF\xFF\xFF\xFF\x00\x00\x00\x00\x00\x00\x00\x00\xFF\xFF\xFF\xFC"letb="\xB3\x31\x2F\xA7\xE2\x3E\xE7\xE4\x98\x8E\x05\x6B\xE3\xF8\x2D\x19\x18\x1D\x9C\x6E\xFE\x81\x41\x12\x03\x14\x08\x8F\x50\x13\x87\x5A\xC6\x56\x39\x8D\x8A\x2E\xD1\x9D\x2A\x85\xC8\xED\xD3\xEC\x2A\xEF"letg_x="\xAA\x87\xCA\x22\xBE\x8B\x05\x37\x8E\xB1\xC7\x1E\xF3\x20\xAD\x74\x6E\x1D\x3B\x62\x8B\xA7\x9B\x98\x59\xF7\x41\xE0\x82\x54\x2A\x38\x55\x02\xF2\x5D\xBF\x55\x29\x6C\x3A\x54\x5E\x38\x72\x76\x0A\xB7"letg_y="\x36\x17\xde\x4a\x96\x26\x2c\x6f\x5d\x9e\x98\xbf\x92\x92\xdc\x29\xf8\xf4\x1d\xbd\x28\x9a\x14\x7c\xe9\xda\x31\x13\xb5\xf0\xb8\xc0\x0a\x60\xb1\xce\x1d\x7e\x81\x9d\x7a\x43\x1d\x7c\x90\xea\x0e\x5f"letp="\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFE\xFF\xFF\xFF\xFF\x00\x00\x00\x00\x00\x00\x00\x00\xFF\xFF\xFF\xFF"letn="\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xC7\x63\x4D\x81\xF4\x37\x2D\xDF\x58\x1A\x0D\xB2\x48\xB0\xA7\x7A\xEC\xEC\x19\x6A\xCC\xC5\x29\x73"letpident="\x3F\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xBF\xFF\xFF\xFF\xC0\x00\x00\x00\x00\x00\x00\x00\x40\x00\x00\x00"|>rev_string(* (Params.p + 1) / 4*)letbyte_length=48letbit_length=384letfe_length=48letfirst_byte_bits=NoneendmoduleForeign=structexternalmul:out_field_element->field_element->field_element->unit="mc_p384_mul"[@@noalloc]externalsub:out_field_element->field_element->field_element->unit="mc_p384_sub"[@@noalloc]externaladd:out_field_element->field_element->field_element->unit="mc_p384_add"[@@noalloc]externalto_montgomery:out_field_element->field_element->unit="mc_p384_to_montgomery"[@@noalloc]externalfrom_octets:out_field_element->string->unit="mc_p384_from_bytes"[@@noalloc]externalset_one:out_field_element->unit="mc_p384_set_one"[@@noalloc]externalnz:field_element->bool="mc_p384_nz"[@@noalloc]externalsqr:out_field_element->field_element->unit="mc_p384_sqr"[@@noalloc]externalfrom_montgomery:out_field_element->field_element->unit="mc_p384_from_montgomery"[@@noalloc]externalto_octets:bytes->field_element->unit="mc_p384_to_bytes"[@@noalloc]externalinv:out_field_element->field_element->unit="mc_p384_inv"[@@noalloc]externalselect_c:out_field_element->bool->field_element->field_element->unit="mc_p384_select"[@@noalloc]externaldouble_c:out_point->point->unit="mc_p384_point_double"[@@noalloc]externaladd_c:out_point->point->point->unit="mc_p384_point_add"[@@noalloc]externalscalar_mult_base_c:out_point->string->unit="mc_p384_scalar_mult_base"[@@noalloc]endmoduleForeign_n=structexternalmul:out_field_element->field_element->field_element->unit="mc_np384_mul"[@@noalloc]externaladd:out_field_element->field_element->field_element->unit="mc_np384_add"[@@noalloc]externalinv:out_field_element->field_element->unit="mc_np384_inv"[@@noalloc]externalone:out_field_element->unit="mc_np384_one"[@@noalloc]externalfrom_bytes:out_field_element->string->unit="mc_np384_from_bytes"[@@noalloc]externalto_bytes:bytes->field_element->unit="mc_np384_to_bytes"[@@noalloc]externalfrom_montgomery:out_field_element->field_element->unit="mc_np384_from_montgomery"[@@noalloc]externalto_montgomery:out_field_element->field_element->unit="mc_np384_to_montgomery"[@@noalloc]endmoduleP=Make_point(Params)(Foreign)moduleS=Make_scalar(Params)(P)moduleDh=Make_dh(Params)(P)(S)moduleFn=Make_Fn(Params)(Foreign_n)moduleDsa=Make_dsa(Params)(Fn)(P)(S)(Digestif.SHA384)endmoduleP521:Dh_dsa=structmoduleParams=structleta="\x01\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFC"letb="\x00\x51\x95\x3E\xB9\x61\x8E\x1C\x9A\x1F\x92\x9A\x21\xA0\xB6\x85\x40\xEE\xA2\xDA\x72\x5B\x99\xB3\x15\xF3\xB8\xB4\x89\x91\x8E\xF1\x09\xE1\x56\x19\x39\x51\xEC\x7E\x93\x7B\x16\x52\xC0\xBD\x3B\xB1\xBF\x07\x35\x73\xDF\x88\x3D\x2C\x34\xF1\xEF\x45\x1F\xD4\x6B\x50\x3F\x00"letg_x="\x00\xC6\x85\x8E\x06\xB7\x04\x04\xE9\xCD\x9E\x3E\xCB\x66\x23\x95\xB4\x42\x9C\x64\x81\x39\x05\x3F\xB5\x21\xF8\x28\xAF\x60\x6B\x4D\x3D\xBA\xA1\x4B\x5E\x77\xEF\xE7\x59\x28\xFE\x1D\xC1\x27\xA2\xFF\xA8\xDE\x33\x48\xB3\xC1\x85\x6A\x42\x9B\xF9\x7E\x7E\x31\xC2\xE5\xBD\x66"letg_y="\x01\x18\x39\x29\x6a\x78\x9a\x3b\xc0\x04\x5c\x8a\x5f\xb4\x2c\x7d\x1b\xd9\x98\xf5\x44\x49\x57\x9b\x44\x68\x17\xaf\xbd\x17\x27\x3e\x66\x2c\x97\xee\x72\x99\x5e\xf4\x26\x40\xc5\x50\xb9\x01\x3f\xad\x07\x61\x35\x3c\x70\x86\xa2\x72\xc2\x40\x88\xbe\x94\x76\x9f\xd1\x66\x50"letp="\x01\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF"letn="\x01\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFF\xFA\x51\x86\x87\x83\xBF\x2F\x96\x6B\x7F\xCC\x01\x48\xF7\x09\xA5\xD0\x3B\xB5\xC9\xB8\x89\x9C\x47\xAE\xBB\x6F\xB7\x1E\x91\x38\x64\x09"letpident="\x01\x7f\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff"|>rev_stringletbyte_length=66letbit_length=521letfe_length=ifSys.word_size==64then72else68(* TODO: is this congruent with C code? *)letfirst_byte_bits=Some0x01endmoduleForeign=structexternalmul:out_field_element->field_element->field_element->unit="mc_p521_mul"[@@noalloc]externalsub:out_field_element->field_element->field_element->unit="mc_p521_sub"[@@noalloc]externaladd:out_field_element->field_element->field_element->unit="mc_p521_add"[@@noalloc]externalto_montgomery:out_field_element->field_element->unit="mc_p521_to_montgomery"[@@noalloc]externalfrom_octets:out_field_element->string->unit="mc_p521_from_bytes"[@@noalloc]externalset_one:out_field_element->unit="mc_p521_set_one"[@@noalloc]externalnz:field_element->bool="mc_p521_nz"[@@noalloc]externalsqr:out_field_element->field_element->unit="mc_p521_sqr"[@@noalloc]externalfrom_montgomery:out_field_element->field_element->unit="mc_p521_from_montgomery"[@@noalloc]externalto_octets:bytes->field_element->unit="mc_p521_to_bytes"[@@noalloc]externalinv:out_field_element->field_element->unit="mc_p521_inv"[@@noalloc]externalselect_c:out_field_element->bool->field_element->field_element->unit="mc_p521_select"[@@noalloc]externaldouble_c:out_point->point->unit="mc_p521_point_double"[@@noalloc]externaladd_c:out_point->point->point->unit="mc_p521_point_add"[@@noalloc]externalscalar_mult_base_c:out_point->string->unit="mc_p521_scalar_mult_base"[@@noalloc]endmoduleForeign_n=structexternalmul:out_field_element->field_element->field_element->unit="mc_np521_mul"[@@noalloc]externaladd:out_field_element->field_element->field_element->unit="mc_np521_add"[@@noalloc]externalinv:out_field_element->field_element->unit="mc_np521_inv"[@@noalloc]externalone:out_field_element->unit="mc_np521_one"[@@noalloc]externalfrom_bytes:out_field_element->string->unit="mc_np521_from_bytes"[@@noalloc]externalto_bytes:bytes->field_element->unit="mc_np521_to_bytes"[@@noalloc]externalfrom_montgomery:out_field_element->field_element->unit="mc_np521_from_montgomery"[@@noalloc]externalto_montgomery:out_field_element->field_element->unit="mc_np521_to_montgomery"[@@noalloc]endmoduleP=Make_point(Params)(Foreign)moduleS=Make_scalar(Params)(P)moduleDh=Make_dh(Params)(P)(S)moduleFn=Make_Fn(Params)(Foreign_n)moduleDsa=Make_dsa(Params)(Fn)(P)(S)(Digestif.SHA512)endmoduleX25519=struct(* RFC 7748 *)externalx25519_scalar_mult_generic:bytes->string->string->unit="mc_x25519_scalar_mult_generic"[@@noalloc]letkey_len=32letscalar_multin_base=letout=Bytes.createkey_leninx25519_scalar_mult_genericoutin_base;Bytes.unsafe_to_stringouttypesecret=stringletbasepoint=String.initkey_len(function0->'\009'|_->'\000')letpublicpriv=scalar_multprivbasepointletgen_key?compress:_?g()=letsecret=Mirage_crypto_rng.generate?gkey_leninsecret,publicsecretletsecret_of_octets?compress:_s=ifString.lengths=key_lenthenOk(s,publics)elseError`Invalid_lengthletsecret_to_octetss=sletis_zero=letzero=String.makekey_len'\000'infunbuf->String.equalzerobufletkey_exchangesecretpublic=ifString.lengthpublic=key_lenthenletres=scalar_multsecretpublicinifis_zeroresthenError`Low_orderelseOkreselseError`Invalid_lengthendmoduleEd25519=structexternalscalar_mult_base_to_bytes:bytes->string->unit="mc_25519_scalar_mult_base"[@@noalloc]externalreduce_l:bytes->unit="mc_25519_reduce_l"[@@noalloc]externalmuladd:bytes->string->string->string->unit="mc_25519_muladd"[@@noalloc]externaldouble_scalar_mult:bytes->string->string->string->bool="mc_25519_double_scalar_mult"[@@noalloc]externalpub_ok:string->bool="mc_25519_pub_ok"[@@noalloc]letkey_len=32letscalar_mult_base_to_bytesp=lettmp=Bytes.createkey_leninscalar_mult_base_to_bytestmpp;Bytes.unsafe_to_stringtmpletmuladdabc=lettmp=Bytes.createkey_leninmuladdtmpabc;Bytes.unsafe_to_stringtmpletdouble_scalar_multabc=lettmp=Bytes.createkey_leninlets=double_scalar_multtmpabcins,Bytes.unsafe_to_stringtmptypepub=stringtypepriv=stringletsha512datas=letopenDigestif.SHA512inletbuf=Bytes.createdigest_sizeinletctx=List.fold_left(feed_string?off:None?len:None)emptydatasinget_into_bytesctxbuf;buf(* RFC 8032 *)letpublicsecret=(* section 5.1.5 *)(* step 1 *)leth=sha512[secret]in(* step 2 *)lets,rest=Bytes.subh0key_len,Bytes.unsafe_to_string(Bytes.subhkey_len(Bytes.lengthh-key_len))inBytes.set_uint8s0((Bytes.get_uint8s0)land248);Bytes.set_uint8s31(((Bytes.get_uint8s31)land127)lor64);lets=Bytes.unsafe_to_stringsin(* step 3 and 4 *)letpublic=scalar_mult_base_to_bytessinpublic,(s,rest)letpub_of_privsecret=fst(publicsecret)letpriv_of_octetsbuf=ifString.lengthbuf=key_lenthenOkbufelseError`Invalid_lengthletpriv_to_octets(priv:priv)=privletpub_of_octetsbuf=ifString.lengthbuf=key_lenthenifpub_okbufthenOkbufelseError`Not_on_curveelseError`Invalid_lengthletpub_to_octetspub=publetgenerate?g()=letsecret=Mirage_crypto_rng.generate?gkey_leninsecret,pub_of_privsecretletsign~keymsg=(* section 5.1.6 *)letpub,(s,prefix)=publickeyinletr=sha512[prefix;msg]inreduce_lr;letr=Bytes.unsafe_to_stringrinletr_big=scalar_mult_base_to_bytesrinletk=sha512[r_big;pub;msg]inreduce_lk;letk=Bytes.unsafe_to_stringkinlets_out=muladdksrinletres=Bytes.create(key_len+key_len)inBytes.unsafe_blit_stringr_big0res0key_len;Bytes.unsafe_blit_strings_out0reskey_lenkey_len;Bytes.unsafe_to_stringresletverify~keysignature~msg=(* section 5.1.7 *)ifString.lengthsignature=2*key_lenthenletr,s=String.subsignature0key_len,String.subsignaturekey_lenkey_leninlets_smaller_l=(* check s within 0 <= s < L *)lets'=Bytes.make(key_len*2)'\000'inBytes.unsafe_blit_strings0s'0key_len;reduce_ls';lets'=Bytes.unsafe_to_strings'inlets''=s^String.makekey_len'\000'inString.equals''s'inifs_smaller_lthenbeginletk=sha512[r;key;msg]inreduce_lk;letk=Bytes.unsafe_to_stringkinletsuccess,r'=double_scalar_multkkeysinsuccess&&String.equalrr'endelsefalseelsefalseend