src/HOL/Auth/OtwayRees_Bad.thy
changeset 16417 9bc16273c2d4
parent 14238 59b02c1efd01
child 17778 93d7e524417a
equal deleted inserted replaced
16416:6061ae1f90f2 16417:9bc16273c2d4
     5 *)
     5 *)
     6 
     6 
     7 
     7 
     8 header{*The Otway-Rees Protocol: The Faulty BAN Version*}
     8 header{*The Otway-Rees Protocol: The Faulty BAN Version*}
     9 
     9 
    10 theory OtwayRees_Bad = Public:
    10 theory OtwayRees_Bad imports Public begin
    11 
    11 
    12 text{*The FAULTY version omitting encryption of Nonce NB, as suggested on 
    12 text{*The FAULTY version omitting encryption of Nonce NB, as suggested on 
    13 page 247 of
    13 page 247 of
    14   Burrows, Abadi and Needham (1988).  A Logic of Authentication.
    14   Burrows, Abadi and Needham (1988).  A Logic of Authentication.
    15   Proc. Royal Soc. 426
    15   Proc. Royal Soc. 426