17 | MPAIR freemsg freemsg |
17 | MPAIR freemsg freemsg |
18 | CRYPT nat freemsg |
18 | CRYPT nat freemsg |
19 | DECRYPT nat freemsg |
19 | DECRYPT nat freemsg |
20 |
20 |
21 text{*The equivalence relation, which makes encryption and decryption inverses |
21 text{*The equivalence relation, which makes encryption and decryption inverses |
22 provided the keys are the same.*} |
22 provided the keys are the same. |
23 consts msgrel :: "(freemsg * freemsg) set" |
23 |
24 |
24 The first two rules are the desired equations. The next four rules |
25 abbreviation |
|
26 msg_rel :: "[freemsg, freemsg] => bool" (infixl "~~" 50) where |
|
27 "X ~~ Y == (X,Y) \<in> msgrel" |
|
28 |
|
29 notation (xsymbols) |
|
30 msg_rel (infixl "\<sim>" 50) |
|
31 notation (HTML output) |
|
32 msg_rel (infixl "\<sim>" 50) |
|
33 |
|
34 text{*The first two rules are the desired equations. The next four rules |
|
35 make the equations applicable to subterms. The last two rules are symmetry |
25 make the equations applicable to subterms. The last two rules are symmetry |
36 and transitivity.*} |
26 and transitivity.*} |
37 inductive "msgrel" |
27 |
38 intros |
28 inductive_set |
39 CD: "CRYPT K (DECRYPT K X) \<sim> X" |
29 msgrel :: "(freemsg * freemsg) set" |
40 DC: "DECRYPT K (CRYPT K X) \<sim> X" |
30 and msg_rel :: "[freemsg, freemsg] => bool" (infixl "\<sim>" 50) |
41 NONCE: "NONCE N \<sim> NONCE N" |
31 where |
42 MPAIR: "\<lbrakk>X \<sim> X'; Y \<sim> Y'\<rbrakk> \<Longrightarrow> MPAIR X Y \<sim> MPAIR X' Y'" |
32 "X \<sim> Y == (X,Y) \<in> msgrel" |
43 CRYPT: "X \<sim> X' \<Longrightarrow> CRYPT K X \<sim> CRYPT K X'" |
33 | CD: "CRYPT K (DECRYPT K X) \<sim> X" |
44 DECRYPT: "X \<sim> X' \<Longrightarrow> DECRYPT K X \<sim> DECRYPT K X'" |
34 | DC: "DECRYPT K (CRYPT K X) \<sim> X" |
45 SYM: "X \<sim> Y \<Longrightarrow> Y \<sim> X" |
35 | NONCE: "NONCE N \<sim> NONCE N" |
46 TRANS: "\<lbrakk>X \<sim> Y; Y \<sim> Z\<rbrakk> \<Longrightarrow> X \<sim> Z" |
36 | MPAIR: "\<lbrakk>X \<sim> X'; Y \<sim> Y'\<rbrakk> \<Longrightarrow> MPAIR X Y \<sim> MPAIR X' Y'" |
|
37 | CRYPT: "X \<sim> X' \<Longrightarrow> CRYPT K X \<sim> CRYPT K X'" |
|
38 | DECRYPT: "X \<sim> X' \<Longrightarrow> DECRYPT K X \<sim> DECRYPT K X'" |
|
39 | SYM: "X \<sim> Y \<Longrightarrow> Y \<sim> X" |
|
40 | TRANS: "\<lbrakk>X \<sim> Y; Y \<sim> Z\<rbrakk> \<Longrightarrow> X \<sim> Z" |
47 |
41 |
48 |
42 |
49 text{*Proving that it is an equivalence relation*} |
43 text{*Proving that it is an equivalence relation*} |
50 |
44 |
51 lemma msgrel_refl: "X \<sim> X" |
45 lemma msgrel_refl: "X \<sim> X" |