src/HOL/UNITY/Simple/NSP_Bad.thy
changeset 42463 f270e3e18be5
parent 37936 1e4c5015a72e
child 42767 e6d920bea7a6
equal deleted inserted replaced
42462:0fd80c27fdf5 42463:f270e3e18be5
    13 From page 260 of
    13 From page 260 of
    14   Burrows, Abadi and Needham.  A Logic of Authentication.
    14   Burrows, Abadi and Needham.  A Logic of Authentication.
    15   Proc. Royal Soc. 426 (1989).
    15   Proc. Royal Soc. 426 (1989).
    16 *}
    16 *}
    17 
    17 
    18 types state = "event list"
    18 type_synonym state = "event list"
    19 
    19 
    20   (*The spy MAY say anything he CAN say.  We do not expect him to
    20   (*The spy MAY say anything he CAN say.  We do not expect him to
    21     invent new nonces here, but he can also use NS1.  Common to
    21     invent new nonces here, but he can also use NS1.  Common to
    22     all similar protocols.*)
    22     all similar protocols.*)
    23 definition
    23 definition