77 checksum, so that garbage can be detected. |
77 checksum, so that garbage can be detected. |
78 \<close> |
78 \<close> |
79 |
79 |
80 (*<*) |
80 (*<*) |
81 text\<open>Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...\<close> |
81 text\<open>Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...\<close> |
|
82 nonterminal mtuple_args |
82 syntax |
83 syntax |
83 "_MTuple" :: "['a, args] \<Rightarrow> 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)") |
84 "" :: "'a \<Rightarrow> mtuple_args" ("_") |
|
85 "_MTuple_args" :: "'a \<Rightarrow> mtuple_args \<Rightarrow> mtuple_args" ("_,/ _") |
|
86 "_MTuple" :: "['a, mtuple_args] \<Rightarrow> 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)") |
84 syntax_consts |
87 syntax_consts |
85 "_MTuple" == MPair |
88 "_MTuple_args" "_MTuple" \<rightleftharpoons> MPair |
86 translations |
89 translations |
87 "\<lbrace>x, y, z\<rbrace>" == "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>" |
90 "\<lbrace>x, y, z\<rbrace>" \<rightleftharpoons> "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>" |
88 "\<lbrace>x, y\<rbrace>" == "CONST MPair x y" |
91 "\<lbrace>x, y\<rbrace>" \<rightleftharpoons> "CONST MPair x y" |
89 |
92 |
90 |
93 |
91 definition keysFor :: "msg set \<Rightarrow> key set" where |
94 definition keysFor :: "msg set \<Rightarrow> key set" where |
92 \<comment> \<open>Keys useful to decrypt elements of a message set\<close> |
95 \<comment> \<open>Keys useful to decrypt elements of a message set\<close> |
93 "keysFor H == invKey ` {K. \<exists>X. Crypt K X \<in> H}" |
96 "keysFor H == invKey ` {K. \<exists>X. Crypt K X \<in> H}" |