src/HOL/Auth/TLS.thy
changeset 14126 28824746d046
parent 13956 8fe7e12290e1
child 16417 9bc16273c2d4
     1.1 --- a/src/HOL/Auth/TLS.thy	Thu Jul 24 16:35:51 2003 +0200
     1.2 +++ b/src/HOL/Auth/TLS.thy	Thu Jul 24 16:36:29 2003 +0200
     1.3 @@ -41,7 +41,7 @@
     1.4  
     1.5  header{*The TLS Protocol: Transport Layer Security*}
     1.6  
     1.7 -theory TLS = Public:
     1.8 +theory TLS = Public + NatPair:
     1.9  
    1.10  constdefs
    1.11    certificate      :: "[agent,key] => msg"
    1.12 @@ -71,13 +71,25 @@
    1.13    "clientK X" == "sessionK(X, ClientRole)"
    1.14    "serverK X" == "sessionK(X, ServerRole)"
    1.15  
    1.16 -axioms
    1.17 +specification (PRF)
    1.18 +  inj_PRF: "inj PRF"
    1.19    --{*the pseudo-random function is collision-free*}
    1.20 -  inj_PRF:       "inj PRF"
    1.21 +   apply (rule exI [of _ "%(x,y,z). nat2_to_nat(x, nat2_to_nat(y,z))"])
    1.22 +   apply (simp add: inj_on_def) 
    1.23 +   apply (blast dest!: nat2_to_nat_inj [THEN injD]) 
    1.24 +   done
    1.25  
    1.26 +specification (sessionK)
    1.27 +  inj_sessionK: "inj sessionK"
    1.28    --{*sessionK is collision-free; also, no clientK clashes with any serverK.*}
    1.29 -  inj_sessionK:  "inj sessionK"	
    1.30 +   apply (rule exI [of _ 
    1.31 +         "%((x,y,z), r). nat2_to_nat(role_case 0 1 r, 
    1.32 +                           nat2_to_nat(x, nat2_to_nat(y,z)))"])
    1.33 +   apply (simp add: inj_on_def split: role.split) 
    1.34 +   apply (blast dest!: nat2_to_nat_inj [THEN injD]) 
    1.35 +   done
    1.36  
    1.37 +axioms
    1.38    --{*sessionK makes symmetric keys*}
    1.39    isSym_sessionK: "sessionK nonces \<in> symKeys"
    1.40