src/HOL/Auth/TLS.thy
changeset 3519 ab0a9fbed4c0
parent 3515 d8a71f6eaf40
child 3672 56e4365a0c99
     1.1 --- a/src/HOL/Auth/TLS.thy	Mon Jul 14 12:44:09 1997 +0200
     1.2 +++ b/src/HOL/Auth/TLS.thy	Mon Jul 14 12:47:21 1997 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4  Server, who is in charge of all public keys.
     1.5  
     1.6  The model assumes that no fraudulent certificates are present, but it does
     1.7 -assume that some private keys are lost to the spy.
     1.8 +assume that some private keys are to the spy.
     1.9  
    1.10  Abstracted from "The TLS Protocol, Version 1.0" by Tim Dierks and Christopher
    1.11  Allen, Transport Layer Security Working Group, 21 May 1997,
    1.12 @@ -56,14 +56,8 @@
    1.13    (*Clashes with pubK and priK are impossible, but this axiom is needed.*)
    1.14    clientK_range "range clientK <= Compl (range serverK)"
    1.15  
    1.16 -  (*Spy has access to his own key for spoof messages, but Server is secure*)
    1.17 -  Spy_in_lost     "Spy: lost"
    1.18 -  Server_not_lost "Server ~: lost"
    1.19  
    1.20 -
    1.21 -consts  lost :: agent set        (*No need for it to be a variable*)
    1.22 -	tls  :: event list set
    1.23 -
    1.24 +consts    tls :: event list set
    1.25  inductive tls
    1.26    intrs 
    1.27      Nil  (*Initial trace is empty*)
    1.28 @@ -71,7 +65,7 @@
    1.29  
    1.30      Fake (*The spy, an active attacker, MAY say anything he CAN say.*)
    1.31           "[| evs: tls;  B ~= Spy;  
    1.32 -             X: synth (analz (sees lost Spy evs)) |]
    1.33 +             X: synth (analz (sees Spy evs)) |]
    1.34            ==> Says Spy B X # evs : tls"
    1.35  
    1.36      SpyKeys (*The spy may apply clientK & serverK to nonces he's found*)