verdict_parser/x509/
oid.rs

1// Shorthands for OIDs and their equality axioms
2
3use vstd::prelude::*;
4
5pub use crate::asn1::ObjectIdentifierValue;
6pub use crate::asn1::UInt;
7pub use crate::common::VecDeep;
8
9verus! {
10
11/// Map OID names to their values
12/// NOTE: to add a new OID, add an entry here
13/// and also in `gen_oid_axioms` below (if disjointness is required)
14#[allow(unused_macros)]
15#[macro_export]
16macro_rules! oid_name {
17    // Extension names
18    (SUBJECT_KEY_IDENT)     => { [2, 5, 29, 14] };
19    (KEY_USAGE)             => { [2, 5, 29, 15] };
20    (SUBJECT_ALT_NAME)      => { [2, 5, 29, 17] };
21    (BASIC_CONSTRAINTS)     => { [2, 5, 29, 19] };
22    (NAME_CONSTRAINTS)      => { [2, 5, 29, 30] };
23    (CERT_POLICIES)         => { [2, 5, 29, 32] };
24    (AUTH_KEY_IDENT)        => { [2, 5, 29, 35] };
25    (EXTENDED_KEY_USAGE)    => { [2, 5, 29, 37] };
26    (AUTH_INFO_ACCESS)      => { [1, 3, 6, 1, 5, 5, 7, 1, 1] };
27
28    // Signature algorithms
29    (RSA_SIGNATURE_MD2)     => { [1, 2, 840, 113549, 1, 1, 2] };
30    (RSA_SIGNATURE_MD5)     => { [1, 2, 840, 113549, 1, 1, 4] };
31    (RSA_SIGNATURE_SHA1)    => { [1, 2, 840, 113549, 1, 1, 5] };
32    (RSA_SIGNATURE_SHA256)  => { [1, 2, 840, 113549, 1, 1, 11] };
33    (RSA_SIGNATURE_SHA384)  => { [1, 2, 840, 113549, 1, 1, 12] };
34    (RSA_SIGNATURE_SHA512)  => { [1, 2, 840, 113549, 1, 1, 13] };
35    (RSA_SIGNATURE_SHA224)  => { [1, 2, 840, 113549, 1, 1, 14] };
36    (DSA_SIGNATURE)         => { [1, 2, 840, 10040, 4, 1] };
37
38    (ECDSA_SIGNATURE_SHA224) => { [1, 2, 840, 10045, 4, 3, 1] };
39    (ECDSA_SIGNATURE_SHA256) => { [1, 2, 840, 10045, 4, 3, 2] };
40    (ECDSA_SIGNATURE_SHA384) => { [1, 2, 840, 10045, 4, 3, 3] };
41    (ECDSA_SIGNATURE_SHA512) => { [1, 2, 840, 10045, 4, 3, 4] };
42
43    (RSA_ENCRYPTION)        => { [1, 2, 840, 113549, 1, 1, 1] };
44    (EC_PUBLIC_KEY)         => { [1, 2, 840, 10045, 2, 1] };
45
46    // EC curves
47    (EC_P_256)              => { [1, 2, 840, 10045, 3, 1, 7] };
48    (EC_P_384)              => { [1, 3, 132, 0, 34] };
49
50    // Directory names
51    (COMMON_NAME)           => { [2, 5, 4, 3] };
52    (COUNTRY_NAME)          => { [2, 5, 4, 6] };
53    (LOCALITY_NAME)         => { [2, 5, 4, 7] };
54    (STATE_NAME)            => { [2, 5, 4, 8] };
55    (ORGANIZATION_NAME)     => { [2, 5, 4, 10] };
56    (ORGANIZATIONAL_UNIT)   => { [2, 5, 4, 11] };
57    (ORGANIZATIONAL_IDENT)  => { [2, 5, 4, 97] };
58    (STREET_ADDRESS)        => { [2, 5, 4, 9] };
59    (SERIAL_NUMBER)         => { [2, 5, 4, 5] };
60    (GIVEN_NAME)            => { [2, 5, 4, 42] };
61    (POSTAL_CODE)           => { [2, 5, 4, 17] };
62    (SURNAME)               => { [2, 5, 4, 4] };
63    (EMAIL_ADDRESS)         => { [1, 2, 840, 113549, 1, 9, 1] };
64
65    (DOMAIN_COMPONENT)      => { [0, 9, 2342, 19200300, 100, 1, 25] };
66
67    // Extended key usage purposes
68    (SERVER_AUTH)           => { [1, 3, 6, 1, 5, 5, 7, 3, 1] };
69    (CLIENT_AUTH)           => { [1, 3, 6, 1, 5, 5, 7, 3, 2] };
70    (CODE_SIGNING)          => { [1, 3, 6, 1, 5, 5, 7, 3, 3] };
71    (EMAIL_PROTECTION)      => { [1, 3, 6, 1, 5, 5, 7, 3, 4] };
72    (TIME_STAMPING)         => { [1, 3, 6, 1, 5, 5, 7, 3, 8] };
73    (OCSP_SIGNING)          => { [1, 3, 6, 1, 5, 5, 7, 3, 9] };
74}
75pub use oid_name;
76
77// Generate axioms for OID names
78macro_rules! gen_oid_axioms {
79    ($($id:ident)*) => {
80        // Generate an axiom saying that the OIDs defined above are all disjoint
81        gen_lemma_disjoint! {
82            axiom_disjoint_oids {
83                $(spec_oid!($id),)*
84            }
85        }
86    };
87}
88
89gen_oid_axioms! {
90    SUBJECT_KEY_IDENT
91    KEY_USAGE
92    SUBJECT_ALT_NAME
93    BASIC_CONSTRAINTS
94    NAME_CONSTRAINTS
95    CERT_POLICIES
96    AUTH_KEY_IDENT
97    EXTENDED_KEY_USAGE
98    RSA_SIGNATURE_MD2
99    RSA_SIGNATURE_MD5
100    RSA_SIGNATURE_SHA1
101    RSA_SIGNATURE_SHA256
102    RSA_SIGNATURE_SHA384
103    RSA_SIGNATURE_SHA512
104    RSA_SIGNATURE_SHA224
105    DSA_SIGNATURE
106    ECDSA_SIGNATURE_SHA224
107    ECDSA_SIGNATURE_SHA256
108    ECDSA_SIGNATURE_SHA384
109    ECDSA_SIGNATURE_SHA512
110    RSA_ENCRYPTION
111    EC_PUBLIC_KEY
112}
113
114impl ObjectIdentifierValue {
115    pub fn from_slice(slice: &[UInt]) -> (res: Self)
116        ensures res@ =~= slice@
117    {
118        ObjectIdentifierValue(VecDeep::from_slice(slice))
119    }
120}
121
122/// Macro for constructing an OID
123#[allow(unused_macros)]
124#[macro_export]
125macro_rules! oid {
126    ($($x:literal),+) => {
127        ObjectIdentifierValue::from_slice(&[$($x),+])
128    };
129
130    ($id:ident) => {
131        ObjectIdentifierValue::from_slice(&oid_name!($id))
132    };
133}
134pub use oid;
135
136#[allow(unused_macros)]
137#[macro_export]
138macro_rules! spec_oid {
139    ($($x:literal),+) => {{
140        // Convert from slice so that we don't need to
141        // assert trivial facts such as oid!(...)@ == spec_oid!(...)
142        let oid: Seq<UInt> = [$($x),+].view();
143        oid
144    }};
145
146    ($id:ident) => {{
147        let oid: Seq<UInt> = oid_name!($id).view();
148        oid
149    }};
150}
151pub use spec_oid;
152
153/// Used to suppress Verus warning about broadcast missing triggers
154pub uninterp spec fn lemma_disjoint_trigger() -> bool;
155
156/// Macro to generate a lemma that states the disjointness of a list of spec terms
157/// NOTE: the disjointness of the provided terms are trusted
158/// incorrect calls to this might lead to unsoundness
159#[allow(unused_macros)]
160#[macro_export]
161macro_rules! gen_lemma_disjoint {
162    ($name:ident { $($term:expr),* $(,)? }) => {
163        ::builtin_macros::verus! {
164            pub broadcast proof fn $name()
165                ensures
166                    (true || #[trigger] lemma_disjoint_trigger()),
167                    gen_lemma_disjoint_helper! {; $($term),* }
168            {}
169        }
170    };
171}
172pub use gen_lemma_disjoint;
173
174#[allow(unused_macros)]
175#[macro_export]
176macro_rules! gen_lemma_disjoint_helper {
177    ($($term:expr),* ; ) => { true };
178
179    ($($prev_term:expr),* ; $term:expr $(, $rest_term:expr)*) => {
180        $(::builtin_macros::verus_proof_expr! { $prev_term != $term } &&)* true && gen_lemma_disjoint_helper!($($prev_term,)* $term ; $($rest_term),*)
181    };
182}
183pub use gen_lemma_disjoint_helper;
184
185}
verdict_parser/x509/oid.rs

verdict_parser/x509/
oid.rs
