src/HOL/Auth/Yahalom.thy
changeset 3961 6a8996fb7d99
parent 3683 aafe719dff14
child 4537 4e835bd9fada
--- a/src/HOL/Auth/Yahalom.thy	Tue Oct 21 10:36:23 1997 +0200
+++ b/src/HOL/Auth/Yahalom.thy	Tue Oct 21 10:39:27 1997 +0200
@@ -49,7 +49,8 @@
                 # evs3 : yahalom"
 
          (*Alice receives the Server's (?) message, checks her Nonce, and
-           uses the new session key to send Bob his Nonce.*)
+           uses the new session key to send Bob his Nonce.  The premise
+           A ~= Server is needed to prove Says_Server_message_form.*)
     YM4  "[| evs4: yahalom;  A ~= Server;  
              Says S A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|},
                         X|}  : set evs4;