56 |
56 |
57 subsubsection{*The Set of Nonces*} |
57 subsubsection{*The Set of Nonces*} |
58 |
58 |
59 text{*A function to return the set of nonces present in a message. It will |
59 text{*A function to return the set of nonces present in a message. It will |
60 be lifted to the initial algrebra, to serve as an example of that process.*} |
60 be lifted to the initial algrebra, to serve as an example of that process.*} |
61 consts |
61 primrec freenonces :: "freemsg \<Rightarrow> nat set" where |
62 freenonces :: "freemsg \<Rightarrow> nat set" |
62 "freenonces (NONCE N) = {N}" |
63 |
63 | "freenonces (MPAIR X Y) = freenonces X \<union> freenonces Y" |
64 primrec |
64 | "freenonces (CRYPT K X) = freenonces X" |
65 "freenonces (NONCE N) = {N}" |
65 | "freenonces (DECRYPT K X) = freenonces X" |
66 "freenonces (MPAIR X Y) = freenonces X \<union> freenonces Y" |
|
67 "freenonces (CRYPT K X) = freenonces X" |
|
68 "freenonces (DECRYPT K X) = freenonces X" |
|
69 |
66 |
70 text{*This theorem lets us prove that the nonces function respects the |
67 text{*This theorem lets us prove that the nonces function respects the |
71 equivalence relation. It also helps us prove that Nonce |
68 equivalence relation. It also helps us prove that Nonce |
72 (the abstract constructor) is injective*} |
69 (the abstract constructor) is injective*} |
73 theorem msgrel_imp_eq_freenonces: "U \<sim> V \<Longrightarrow> freenonces U = freenonces V" |
70 theorem msgrel_imp_eq_freenonces: "U \<sim> V \<Longrightarrow> freenonces U = freenonces V" |
76 |
73 |
77 subsubsection{*The Left Projection*} |
74 subsubsection{*The Left Projection*} |
78 |
75 |
79 text{*A function to return the left part of the top pair in a message. It will |
76 text{*A function to return the left part of the top pair in a message. It will |
80 be lifted to the initial algrebra, to serve as an example of that process.*} |
77 be lifted to the initial algrebra, to serve as an example of that process.*} |
81 consts freeleft :: "freemsg \<Rightarrow> freemsg" |
78 primrec freeleft :: "freemsg \<Rightarrow> freemsg" where |
82 primrec |
79 "freeleft (NONCE N) = NONCE N" |
83 "freeleft (NONCE N) = NONCE N" |
80 | "freeleft (MPAIR X Y) = X" |
84 "freeleft (MPAIR X Y) = X" |
81 | "freeleft (CRYPT K X) = freeleft X" |
85 "freeleft (CRYPT K X) = freeleft X" |
82 | "freeleft (DECRYPT K X) = freeleft X" |
86 "freeleft (DECRYPT K X) = freeleft X" |
|
87 |
83 |
88 text{*This theorem lets us prove that the left function respects the |
84 text{*This theorem lets us prove that the left function respects the |
89 equivalence relation. It also helps us prove that MPair |
85 equivalence relation. It also helps us prove that MPair |
90 (the abstract constructor) is injective*} |
86 (the abstract constructor) is injective*} |
91 theorem msgrel_imp_eqv_freeleft: |
87 theorem msgrel_imp_eqv_freeleft: |
94 |
90 |
95 |
91 |
96 subsubsection{*The Right Projection*} |
92 subsubsection{*The Right Projection*} |
97 |
93 |
98 text{*A function to return the right part of the top pair in a message.*} |
94 text{*A function to return the right part of the top pair in a message.*} |
99 consts freeright :: "freemsg \<Rightarrow> freemsg" |
95 primrec freeright :: "freemsg \<Rightarrow> freemsg" where |
100 primrec |
96 "freeright (NONCE N) = NONCE N" |
101 "freeright (NONCE N) = NONCE N" |
97 | "freeright (MPAIR X Y) = Y" |
102 "freeright (MPAIR X Y) = Y" |
98 | "freeright (CRYPT K X) = freeright X" |
103 "freeright (CRYPT K X) = freeright X" |
99 | "freeright (DECRYPT K X) = freeright X" |
104 "freeright (DECRYPT K X) = freeright X" |
|
105 |
100 |
106 text{*This theorem lets us prove that the right function respects the |
101 text{*This theorem lets us prove that the right function respects the |
107 equivalence relation. It also helps us prove that MPair |
102 equivalence relation. It also helps us prove that MPair |
108 (the abstract constructor) is injective*} |
103 (the abstract constructor) is injective*} |
109 theorem msgrel_imp_eqv_freeright: |
104 theorem msgrel_imp_eqv_freeright: |
112 |
107 |
113 |
108 |
114 subsubsection{*The Discriminator for Constructors*} |
109 subsubsection{*The Discriminator for Constructors*} |
115 |
110 |
116 text{*A function to distinguish nonces, mpairs and encryptions*} |
111 text{*A function to distinguish nonces, mpairs and encryptions*} |
117 consts freediscrim :: "freemsg \<Rightarrow> int" |
112 primrec freediscrim :: "freemsg \<Rightarrow> int" where |
118 primrec |
113 "freediscrim (NONCE N) = 0" |
119 "freediscrim (NONCE N) = 0" |
114 | "freediscrim (MPAIR X Y) = 1" |
120 "freediscrim (MPAIR X Y) = 1" |
115 | "freediscrim (CRYPT K X) = freediscrim X + 2" |
121 "freediscrim (CRYPT K X) = freediscrim X + 2" |
116 | "freediscrim (DECRYPT K X) = freediscrim X - 2" |
122 "freediscrim (DECRYPT K X) = freediscrim X - 2" |
|
123 |
117 |
124 text{*This theorem helps us prove @{term "Nonce N \<noteq> MPair X Y"}*} |
118 text{*This theorem helps us prove @{term "Nonce N \<noteq> MPair X Y"}*} |
125 theorem msgrel_imp_eq_freediscrim: |
119 theorem msgrel_imp_eq_freediscrim: |
126 "U \<sim> V \<Longrightarrow> freediscrim U = freediscrim V" |
120 "U \<sim> V \<Longrightarrow> freediscrim U = freediscrim V" |
127 by (induct set: msgrel) auto |
121 by (induct set: msgrel) auto |