# HG changeset patch # User paulson # Date 866641115 -7200 # Node ID c7c8c0db05b98fe4af6afcd4d25e9b8cca9798bb # Parent a14e5451f613f40b57f68ae300e7e184d1a7b2e0 Defines KeyWithNonce, which is used to prove the secrecy of NB diff -r a14e5451f613 -r c7c8c0db05b9 src/HOL/Auth/Yahalom.thy --- a/src/HOL/Auth/Yahalom.thy Wed Jun 18 15:31:31 1997 +0200 +++ b/src/HOL/Auth/Yahalom.thy Wed Jun 18 15:38:35 1997 +0200 @@ -44,9 +44,9 @@ {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} : set_of_list evs |] ==> Says Server A - {|Crypt (shrK A) {|Agent B, Key KAB, Nonce NA, Nonce NB|}, - Crypt (shrK B) {|Agent A, Key KAB|}|} - # evs : yahalom lost" + {|Crypt (shrK A) {|Agent B, Key KAB, Nonce NA, Nonce NB|}, + Crypt (shrK B) {|Agent A, Key KAB|}|} + # evs : yahalom lost" (*Alice receives the Server's (?) message, checks her Nonce, and uses the new session key to send Bob his Nonce.*) @@ -65,4 +65,12 @@ X|} : set_of_list evs |] ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : yahalom lost" + +constdefs + KeyWithNonce :: [key, nat, event list] => bool + "KeyWithNonce K NB evs == + EX A B na X. + Says Server A {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|} + : set_of_list evs" + end