src/HOL/Auth/Shared.thy
changeset 2376 f5c61fd9b9b6
parent 2319 95f0d5243c85
child 2451 ce85a2aafc7a
     1.1 --- a/src/HOL/Auth/Shared.thy	Fri Dec 13 10:20:55 1996 +0100
     1.2 +++ b/src/HOL/Auth/Shared.thy	Fri Dec 13 10:42:58 1996 +0100
     1.3 @@ -44,19 +44,24 @@
     1.4    sees_Cons "sees lost A (ev#evs) = sees1 A ev Un sees lost A evs"
     1.5  
     1.6  
     1.7 -(*Agents generate "random" nonces and keys.  These are uniquely determined by
     1.8 -  the length of their argument, a trace.*)
     1.9 +(*Agents generate "random" numbers for use as symmetric keys, as well as
    1.10 +  nonces.*)
    1.11 +
    1.12  consts
    1.13 -  newN :: "event list => nat"
    1.14 -  newK :: "event list => key"
    1.15 +  random :: "nat*nat => nat"
    1.16 +
    1.17 +constdefs
    1.18 +  newN   :: event list => nat
    1.19 +  "newN evs == random (length evs, 0)"
    1.20 +
    1.21 +  newK   :: event list => nat
    1.22 +  "newK evs == random (length evs, 1)"
    1.23  
    1.24  rules
    1.25 -  inj_shrK      "inj shrK"
    1.26 +  inj_shrK        "inj shrK"
    1.27 +  inj_random      "inj random"
    1.28  
    1.29 -  newN_length   "(newN evs = newN evt) ==> (length evs = length evt)"
    1.30 -  newK_length   "(newK evs = newK evt) ==> (length evs = length evt)"
    1.31 -
    1.32 -  newK_neq_shrK "newK evs ~= shrK A" 
    1.33 -  isSym_newK    "isSymKey (newK evs)"
    1.34 +  random_neq_shrK "random ij ~= shrK A" 
    1.35 +  isSym_random    "isSymKey (random ij)"
    1.36  
    1.37  end