vest_lib/asn1/
der.rs

1//! Canonical DER universal formats and notation-style constructors.
2//!
3//! Constants such as `INTEGER`, `OCTET_STRING`, and `SEQUENCE` combine ASN.1
4//! tags with canonical content formats. DER rejects alternative BER encodings
5//! and therefore supports non-malleability when its children do.
6use super::modifiers::{defaulted, explicit_tag};
7pub use super::modifiers::{
8    implicitly_tagged as Implicit, ImplicitFmt, CHOICE, IMPLICIT, IMPLICIT_APPLICATION,
9    IMPLICIT_PRIVATE, OPTIONAL, REQUIRED,
10};
11use super::{
12    ASN1Fmt, AnyFmt, BitStringFmt, BmpStringFmt, BoolFmt, Class, EnumeratedFmt, GeneralizedTimeFmt,
13    Ia5StringFmt, Integer16Fmt, Integer8Fmt, IntegerFmt, NullFmt, NumericStringFmt,
14    ObjectIdentifierFmt, OctetStringFmt, PrintableStringFmt, RealFmt, SetOfFmt, TagFmt,
15    TeletexStringFmt, UniversalStringFmt, UtcTimeFmt, Utf8StringFmt, DER,
16};
17use crate::core::{proof::*, spec::*};
18use vstd::prelude::*;
19
20verus! {
21
22/// Uniform notation aliases used by schema generators.
23pub type BoolTlvFmt = ASN1Fmt<BoolFmt<DER>, DER>;
24
25pub type AnyTlvFmt = AnyFmt<DER>;
26
27pub type IntegerTlvFmt = ASN1Fmt<IntegerFmt, DER>;
28
29pub type Integer8TlvFmt = ASN1Fmt<Integer8Fmt, DER>;
30
31pub type Integer16TlvFmt = ASN1Fmt<Integer16Fmt, DER>;
32
33pub type EnumeratedTlvFmt = ASN1Fmt<EnumeratedFmt, DER>;
34
35pub type Enumerated16TlvFmt = ASN1Fmt<Integer16Fmt, DER>;
36
37pub type ObjectIdentifierTlvFmt = ASN1Fmt<ObjectIdentifierFmt, DER>;
38
39pub type RealTlvFmt = ASN1Fmt<RealFmt<DER>, DER>;
40
41pub type BitStringTlvFmt = ASN1Fmt<BitStringFmt<DER>, DER>;
42
43pub type OctetStringTlvFmt = ASN1Fmt<OctetStringFmt, DER>;
44
45pub type NullTlvFmt = ASN1Fmt<NullFmt, DER>;
46
47pub type Utf8StringTlvFmt = ASN1Fmt<Utf8StringFmt, DER>;
48
49pub type PrintableStringTlvFmt = ASN1Fmt<PrintableStringFmt, DER>;
50
51pub type NumericStringTlvFmt = ASN1Fmt<NumericStringFmt, DER>;
52
53pub type TeletexStringTlvFmt = ASN1Fmt<TeletexStringFmt, DER>;
54
55pub type Ia5StringTlvFmt = ASN1Fmt<Ia5StringFmt, DER>;
56
57pub type UtcTimeTlvFmt = ASN1Fmt<UtcTimeFmt<DER>, DER>;
58
59pub type GeneralizedTimeTlvFmt = ASN1Fmt<GeneralizedTimeFmt<DER>, DER>;
60
61pub type BmpStringTlvFmt = ASN1Fmt<BmpStringFmt, DER>;
62
63pub type UniversalStringTlvFmt = ASN1Fmt<UniversalStringFmt, DER>;
64
65pub type SequenceFmt<C> = ASN1Fmt<C, DER>;
66
67pub type SetFmt<C> = ASN1Fmt<C, DER>;
68
69pub type SequenceOfFmt<C> = ASN1Fmt<crate::combinators::RepeatTillEnd<C>, DER>;
70
71pub type SetOfTlvFmt<C> = ASN1Fmt<SetOfFmt<C>, DER>;
72
73pub type ExplicitFmt<C> = ASN1Fmt<C, DER>;
74
75pub type DefaultFmt<Field, Default, Rest> = super::DefaultedFmt<Field, Default, Rest, DER>;
76
77pub type Eof = crate::combinators::Eof;
78
79#[allow(non_upper_case_globals)]
80pub const Eof: Eof = crate::combinators::Eof;
81
82pub const BOOLEAN: BoolTlvFmt = ASN1Fmt(TagFmt::BOOLEAN, BoolFmt::<DER>);
83
84pub const ANY: AnyTlvFmt = AnyFmt::<DER>;
85
86pub const INTEGER: IntegerTlvFmt = ASN1Fmt(TagFmt::INTEGER, IntegerFmt);
87
88pub const INTEGER8: Integer8TlvFmt = ASN1Fmt(TagFmt::INTEGER, Integer8Fmt);
89
90pub const INTEGER16: Integer16TlvFmt = ASN1Fmt(TagFmt::INTEGER, Integer16Fmt);
91
92pub const ENUMERATED: EnumeratedTlvFmt = ASN1Fmt(TagFmt::ENUMERATED, EnumeratedFmt);
93
94pub const ENUMERATED16: Enumerated16TlvFmt = ASN1Fmt(TagFmt::ENUMERATED, Integer16Fmt);
95
96pub const OBJECT_IDENTIFIER: ObjectIdentifierTlvFmt = ASN1Fmt(
97    TagFmt::OBJECT_IDENTIFIER,
98    ObjectIdentifierFmt,
99);
100
101pub const REAL: RealTlvFmt = ASN1Fmt(TagFmt::REAL, RealFmt::<DER>);
102
103pub const BIT_STRING: BitStringTlvFmt = ASN1Fmt(TagFmt::BIT_STRING, BitStringFmt::<DER>);
104
105pub const OCTET_STRING: OctetStringTlvFmt = ASN1Fmt(TagFmt::OCTET_STRING, OctetStringFmt);
106
107pub const NULL: NullTlvFmt = ASN1Fmt(TagFmt::NULL, NullFmt);
108
109pub const UTF8_STRING: Utf8StringTlvFmt = ASN1Fmt(TagFmt::UTF8_STRING, Utf8StringFmt);
110
111pub const PRINTABLE_STRING: PrintableStringTlvFmt = ASN1Fmt(
112    TagFmt::PRINTABLE_STRING,
113    PrintableStringFmt,
114);
115
116pub const NUMERIC_STRING: NumericStringTlvFmt = ASN1Fmt(TagFmt::NUMERIC_STRING, NumericStringFmt);
117
118pub const TELETEX_STRING: TeletexStringTlvFmt = ASN1Fmt(TagFmt::TELETEX_STRING, TeletexStringFmt);
119
120pub const IA5_STRING: Ia5StringTlvFmt = ASN1Fmt(TagFmt::IA5_STRING, Ia5StringFmt);
121
122pub const UTC_TIME: UtcTimeTlvFmt = ASN1Fmt(TagFmt::UTC_TIME, UtcTimeFmt::<DER>);
123
124pub const GENERALIZED_TIME: GeneralizedTimeTlvFmt = ASN1Fmt(
125    TagFmt::GENERALIZED_TIME,
126    GeneralizedTimeFmt::<DER>,
127);
128
129pub const BMP_STRING: BmpStringTlvFmt = ASN1Fmt(TagFmt::BMP_STRING, BmpStringFmt);
130
131pub const UNIVERSAL_STRING: UniversalStringTlvFmt = ASN1Fmt(
132    TagFmt::UNIVERSAL_STRING,
133    UniversalStringFmt,
134);
135
136/// Construct a DER `SET OF` whose elements are complete DER formats.
137#[allow(non_snake_case)]
138#[verifier::allow_in_spec]
139pub const fn SET_OF<C: Copy>(inner: C) -> SetOfTlvFmt<C>
140    returns
141        ASN1Fmt::<SetOfFmt<C>, DER>(TagFmt::SET, SetOfFmt(inner)),
142{
143    ASN1Fmt::<SetOfFmt<C>, DER>(TagFmt::SET, SetOfFmt(inner))
144}
145
146/// Construct a DER `SEQUENCE` format.
147#[allow(non_snake_case)]
148#[verifier::allow_in_spec]
149pub const fn SEQUENCE<C: Copy>(inner: C) -> SequenceFmt<C>
150    returns
151        ASN1Fmt::<C, DER>(TagFmt::SEQUENCE, inner),
152{
153    ASN1Fmt::<C, DER>(TagFmt::SEQUENCE, inner)
154}
155
156/// Construct a DER `SET` whose component chain is already in canonical tag order.
157#[allow(non_snake_case)]
158#[verifier::allow_in_spec]
159pub const fn SET<C: Copy>(inner: C) -> SetFmt<C>
160    returns
161        ASN1Fmt::<C, DER>(TagFmt::SET, inner),
162{
163    ASN1Fmt::<C, DER>(TagFmt::SET, inner)
164}
165
166/// Construct a DER `SEQUENCE OF` whose elements are complete DER formats.
167#[allow(non_snake_case)]
168#[verifier::allow_in_spec]
169pub const fn SEQUENCE_OF<C: Copy>(inner: C) -> SequenceOfFmt<C>
170    returns
171        ASN1Fmt::<crate::combinators::RepeatTillEnd<C>, DER>(
172            TagFmt::SEQUENCE,
173            crate::combinators::RepeatTillEnd(inner),
174        ),
175{
176    ASN1Fmt::<crate::combinators::RepeatTillEnd<C>, DER>(
177        TagFmt::SEQUENCE,
178        crate::combinators::RepeatTillEnd(inner),
179    )
180}
181
182/// Apply an ASN.1 EXPLICIT tag with an arbitrary tag class.
183#[allow(non_snake_case)]
184#[verifier::allow_in_spec]
185pub const fn Explicit<C: Copy>(class: Class, number: u64, inner: C) -> ExplicitFmt<C>
186    returns
187        ASN1Fmt::<C, DER>(explicit_tag(class, number), inner),
188{
189    ASN1Fmt(explicit_tag(class, number), inner)
190}
191
192/// Apply an ASN.1 context-specific EXPLICIT tag to a DER-encoded format.
193#[allow(non_snake_case)]
194#[verifier::allow_in_spec]
195pub const fn EXPLICIT<C: Copy>(number: u64, inner: C) -> ExplicitFmt<C>
196    returns
197        Explicit(Class::ContextSpecific, number, inner),
198{
199    Explicit(Class::ContextSpecific, number, inner)
200}
201
202/// Apply an ASN.1 application-class EXPLICIT tag to a DER-encoded format.
203#[allow(non_snake_case)]
204#[verifier::allow_in_spec]
205pub const fn EXPLICIT_APPLICATION<C: Copy>(number: u64, inner: C) -> ExplicitFmt<C>
206    returns
207        Explicit(Class::Application, number, inner),
208{
209    Explicit(Class::Application, number, inner)
210}
211
212/// Apply an ASN.1 private-class EXPLICIT tag to a DER-encoded format.
213#[allow(non_snake_case)]
214#[verifier::allow_in_spec]
215pub const fn EXPLICIT_PRIVATE<C: Copy>(number: u64, inner: C) -> ExplicitFmt<C>
216    returns
217        Explicit(Class::Private, number, inner),
218{
219    Explicit(Class::Private, number, inner)
220}
221
222/// The `DEFAULT` modifier for DER-encoded formats.
223#[allow(non_snake_case)]
224#[verifier::allow_in_spec]
225pub const fn DEFAULT<Field, Rest>(field: Field, default: Field::T, cont: Rest) -> DefaultFmt<
226    Field,
227    Field::T,
228    Rest,
229> where Field: SpecByteLen
230    returns
231        defaulted::<Field, Rest, DER>(field, default, cont),
232{
233    defaulted::<Field, Rest, DER>(field, default, cont)
234}
235
236} // verus!
237verus! {
238
239use crate::combinators::{Choice, Optional, Pair};
240
241#[verifier::allow_in_spec]
242#[allow(non_snake_case)]
243const fn MY_FMT() -> Pair<
244    IntegerTlvFmt,
245    DefaultFmt<
246        BoolTlvFmt,
247        bool,
248        Pair<
249            BitStringTlvFmt,
250            Optional<
251                OctetStringTlvFmt,
252                DefaultFmt<Integer8TlvFmt, i8, Optional<UtcTimeTlvFmt, Utf8StringTlvFmt>>,
253            >,
254        >,
255    >,
256>
257    returns
258        REQUIRED(
259            INTEGER,
260            DEFAULT(
261                BOOLEAN,
262                false,
263                REQUIRED(
264                    BIT_STRING,
265                    OPTIONAL(OCTET_STRING, DEFAULT(INTEGER8, 0, OPTIONAL(UTC_TIME, UTF8_STRING))),
266                ),
267            ),
268        ),
269{
270    REQUIRED(
271        INTEGER,
272        DEFAULT(
273            BOOLEAN,
274            false,
275            REQUIRED(
276                BIT_STRING,
277                OPTIONAL(OCTET_STRING, DEFAULT(INTEGER8, 0, OPTIONAL(UTC_TIME, UTF8_STRING))),
278            ),
279        ),
280    )
281}
282
283#[verifier::allow_in_spec]
284#[allow(non_snake_case)]
285const fn MY_FMT2() -> Pair<
286    IntegerTlvFmt,
287    DefaultFmt<
288        ExplicitFmt<Integer16TlvFmt>,
289        i16,
290        Optional<
291            ImplicitFmt<Integer16TlvFmt>,
292            Optional<
293                ImplicitFmt<Integer16TlvFmt>,
294                DefaultFmt<
295                    ExplicitFmt<Integer16TlvFmt>,
296                    i16,
297                    Optional<UtcTimeTlvFmt, Utf8StringTlvFmt>,
298                >,
299            >,
300        >,
301    >,
302>
303    returns
304        REQUIRED(
305            INTEGER,
306            DEFAULT(
307                EXPLICIT(0, INTEGER16),
308                10,
309                OPTIONAL(
310                    IMPLICIT(1, INTEGER16),
311                    OPTIONAL(
312                        IMPLICIT(2, INTEGER16),
313                        DEFAULT(EXPLICIT(3, INTEGER16), 0, OPTIONAL(UTC_TIME, UTF8_STRING)),
314                    ),
315                ),
316            ),
317        ),
318{
319    REQUIRED(
320        INTEGER,
321        DEFAULT(
322            EXPLICIT(0, INTEGER16),
323            10,
324            OPTIONAL(
325                IMPLICIT(1, INTEGER16),
326                OPTIONAL(
327                    IMPLICIT(2, INTEGER16),
328                    DEFAULT(EXPLICIT(3, INTEGER16), 0, OPTIONAL(UTC_TIME, UTF8_STRING)),
329                ),
330            ),
331        ),
332    )
333}
334
335proof fn chain_of_optional_defaulted() {
336    use crate::combinators::disjoint::disjointness_lemmas;
337    use super::disjoint::asn1_disjointness_lemmas;
338
339    broadcast use disjointness_lemmas;
340    broadcast use asn1_disjointness_lemmas;
341
342    assert(MY_FMT().safe_inv());
343    assert(MY_FMT().sound_inv());
344    assert(MY_FMT().unambiguous());
345    assert(MY_FMT().nonmal_inv());
346
347    assert(MY_FMT2().safe_inv());
348    assert(MY_FMT2().sound_inv());
349    assert(MY_FMT2().unambiguous());
350    assert(MY_FMT2().nonmal_inv());
351
352    #[verusfmt::skip]
353    let fmt =
354        REQUIRED (INTEGER,
355        DEFAULT  (BOOLEAN, false,
356        REQUIRED (BIT_STRING,
357        OPTIONAL (OCTET_STRING,
358        DEFAULT  (INTEGER8, 0,
359        OPTIONAL (UTC_TIME, UTF8_STRING))))));
360
361    assert(fmt.safe_inv());
362    assert(fmt.sound_inv());
363    assert(fmt.unambiguous());
364
365    #[verusfmt::skip]
366    let fmt1 =
367        REQUIRED  (INTEGER,
368        DEFAULT   (EXPLICIT (0, INTEGER16), 10,
369        OPTIONAL  (IMPLICIT (1, INTEGER16),
370        OPTIONAL  (IMPLICIT (2, INTEGER16),
371        DEFAULT   (EXPLICIT (3, INTEGER16), 0,
372        OPTIONAL  (UTC_TIME, UTF8_STRING))))));
373
374    assert(fmt1.safe_inv());
375    assert(fmt1.sound_inv());
376    assert(fmt1.unambiguous());
377
378    #[verusfmt::skip]
379    let fmt2 = CHOICE(
380        IMPLICIT (0, NULL),     CHOICE(
381        IMPLICIT (1, NULL),     CHOICE(
382        IMPLICIT (2, INTEGER8), CHOICE(
383        EXPLICIT (3, INTEGER8), CHOICE(
384        OCTET_STRING, UTF8_STRING)))));
385
386    assert(fmt2.safe_inv());
387    assert(fmt2.sound_inv());
388    assert(fmt2.unambiguous());
389}
390
391} // verus!
vest_lib/asn1/der.rs

vest_lib/asn1/
der.rs
