Defines KeyWithNonce, which is used to prove the secrecy of NB
authorpaulson
Wed Jun 18 15:38:35 1997 +0200 (1997-06-18)
changeset 3447c7c8c0db05b9
parent 3446 a14e5451f613
child 3448 8a79e27ac53b
Defines KeyWithNonce, which is used to prove the secrecy of NB
src/HOL/Auth/Yahalom.thy
     1.1 --- a/src/HOL/Auth/Yahalom.thy	Wed Jun 18 15:31:31 1997 +0200
     1.2 +++ b/src/HOL/Auth/Yahalom.thy	Wed Jun 18 15:38:35 1997 +0200
     1.3 @@ -44,9 +44,9 @@
     1.4                    {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
     1.5                 : set_of_list evs |]
     1.6            ==> Says Server A
     1.7 -                  {|Crypt (shrK A) {|Agent B, Key KAB, Nonce NA, Nonce NB|},
     1.8 -                    Crypt (shrK B) {|Agent A, Key KAB|}|}
     1.9 -                 # evs : yahalom lost"
    1.10 +                   {|Crypt (shrK A) {|Agent B, Key KAB, Nonce NA, Nonce NB|},
    1.11 +                     Crypt (shrK B) {|Agent A, Key KAB|}|}
    1.12 +                # evs : yahalom lost"
    1.13  
    1.14           (*Alice receives the Server's (?) message, checks her Nonce, and
    1.15             uses the new session key to send Bob his Nonce.*)
    1.16 @@ -65,4 +65,12 @@
    1.17                               X|}  : set_of_list evs |]
    1.18            ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : yahalom lost"
    1.19  
    1.20 +
    1.21 +constdefs 
    1.22 +  KeyWithNonce :: [key, nat, event list] => bool
    1.23 +  "KeyWithNonce K NB evs ==
    1.24 +     EX A B na X. 
    1.25 +       Says Server A {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|} 
    1.26 +         : set_of_list evs"
    1.27 +
    1.28  end