src/HOL/Auth/Yahalom2.thy
changeset 3466 30791e5a69c4
parent 3465 e85c24717cad
child 3481 256f38c01b98
equal deleted inserted replaced
3465:e85c24717cad 3466:30791e5a69c4
    55 
    55 
    56          (*Alice receives the Server's (?) message, checks her Nonce, and
    56          (*Alice receives the Server's (?) message, checks her Nonce, and
    57            uses the new session key to send Bob his Nonce.*)
    57            uses the new session key to send Bob his Nonce.*)
    58     YM4  "[| evs: yahalom lost;  A ~= Server;  A ~= B;  
    58     YM4  "[| evs: yahalom lost;  A ~= Server;  A ~= B;  
    59              Says S A {|Nonce NB, Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
    59              Says S A {|Nonce NB, Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
    60                         X|}
    60                         X|}  : set evs;
    61                : set evs;
       
    62              Says A B {|Agent A, Nonce NA|} : set evs |]
    61              Says A B {|Agent A, Nonce NA|} : set evs |]
    63           ==> Says A B {|X, Crypt K (Nonce NB)|} # evs : yahalom lost"
    62           ==> Says A B {|X, Crypt K (Nonce NB)|} # evs : yahalom lost"
    64 
    63 
    65          (*This message models possible leaks of session keys.  The nonces
    64          (*This message models possible leaks of session keys.  The nonces
    66            identify the protocol run.  Quoting Server here ensures they are
    65            identify the protocol run.  Quoting Server here ensures they are