| changeset 16417 | 9bc16273c2d4 |
| parent 14238 | 59b02c1efd01 |
| child 17778 | 93d7e524417a |
--- a/src/HOL/Auth/OtwayRees_Bad.thy Fri Jun 17 11:35:35 2005 +0200 +++ b/src/HOL/Auth/OtwayRees_Bad.thy Fri Jun 17 16:12:49 2005 +0200 @@ -7,7 +7,7 @@ header{*The Otway-Rees Protocol: The Faulty BAN Version*} -theory OtwayRees_Bad = Public: +theory OtwayRees_Bad imports Public begin text{*The FAULTY version omitting encryption of Nonce NB, as suggested on page 247 of