miTLS
A verified reference TLS implementation
Home
Download
Browse
TLS Attacks
People
miTLS
:: DER
F# Interface: DER.fsi
(* * Copyright (c) 2012--2013 MSR-INRIA Joint Center. All rights reserved. * * This code is distributed under the terms for the CeCILL-B (version 1) * license. * * You should have received a copy of the CeCILL-B (version 1) license * along with this program. If not, see: * * http://www.cecill.info/licences/Licence_CeCILL-B_V1-en.txt *) module DER open Bytes type dervalue = | Bool of bool | Bytes of bytes | Utf8String of string | Sequence of dervalue list exception DerEncodingFailure val encode : dervalue -> bytes val decode : bytes -> dervalue option
F# Implementation: DER.fs
(* * Copyright (c) 2012--2013 MSR-INRIA Joint Center. All rights reserved. * * This code is distributed under the terms for the CeCILL-B (version 1) * license. * * You should have received a copy of the CeCILL-B (version 1) license * along with this program. If not, see: * * http://www.cecill.info/licences/Licence_CeCILL-B_V1-en.txt *) module DER // ------------------------------------------------------------------------ open System open Org.BouncyCastle.Asn1 // ------------------------------------------------------------------------ type dervalue = | Bool of bool | Bytes of byte[] | Utf8String of string | Sequence of dervalue list // ------------------------------------------------------------------------ exception DerEncodingFailure exception DerDecodingFailure // ------------------------------------------------------------------------ let get_asn1_object (bytes : byte[]) : Asn1Object = try let stream = new Asn1InputStream(bytes) let obj = stream.ReadObject() if stream.Position <> int64(bytes.Length) then null else obj with _ -> null // ------------------------------------------------------------------------ let rec encode_r = function | Bytes bytes -> (new DerOctetString(bytes) :> Asn1Encodable) | Utf8String string -> (new DerUtf8String (string) :> Asn1Encodable) | Bool b -> let b = if b then 0xffuy else 0x00uy in ((new DerBoolean [|b|]) :> Asn1Encodable) | Sequence seq -> let seq = seq |> List.map encode_r in (new DerSequence(Array.ofList seq) :> Asn1Encodable) let encode (x : dervalue) = try (encode_r x).GetDerEncoded() with _ -> raise DerEncodingFailure // ------------------------------------------------------------------------ let rec decode_r (o : Asn1Encodable) : dervalue = match o with | (:? DerBoolean as o) -> Bool (o.IsTrue) | (:? DerOctetString as o) -> Bytes (o.GetOctets()) | (:? DerUtf8String as o) -> Utf8String (o.GetString()) | (:? DerSequence as o) -> Sequence ((Seq.cast o) |> Seq.map decode_r |> Seq.toList) | _ -> raise DerDecodingFailure let decode (bytes : byte[]) : dervalue option = try let obj = get_asn1_object bytes in Some (decode_r obj) with _ -> None
F7 Interface: DER.fs7
(* * Copyright (c) 2012--2013 MSR-INRIA Joint Center. All rights reserved. * * This code is distributed under the terms for the CeCILL-B (version 1) * license. * * You should have received a copy of the CeCILL-B (version 1) license * along with this program. If not, see: * * http://www.cecill.info/licences/Licence_CeCILL-B_V1-en.txt *) module DER (* Trivially trusted; used only in sample apps *) open Bytes type dervalue = | Bool of bool | Bytes of bytes | Utf8String of string | Sequence of dervalue list val encode : dervalue -> bytes val decode : bytes -> dervalue option
Verification status
Verification depends on the F7 interfaces of the following modules:
Bytes
Module list
Trusted
SessionDB
Bytes
Cert
Tcp
Range
TLSExtensions
TLSConstants
Idealized
Nonce
PRF
DH
MAC_SHA1
RSA
LHAE
RSAKey
DHGroup
MAC_SHA256
Sig
ENC
CRE
Verified
TLS
UTLS
DataStream
AppData
PwToken
LHAEPlain
TLSInfo
Handshake
StatefulLHAE
Alert
TLSFragment
Record
MAC
Dispatch
Error
Encode
PwApp