src/HOL/Auth/TLS.thy

 	   PA represents CLIENT_VERSION, CIPHER_SUITES and COMPRESSION_METHODS.
 	   It is uninterpreted but will be confirmed in the FINISHED messages.
 	   NA is CLIENT RANDOM, while SID is SESSION_ID.
            UNIX TIME is omitted because the protocol doesn't use it.
            May assume NA ~: range PRF because CLIENT RANDOM is 28 bytes
-	   while MASTER SECRET is 48 byptes*)
+	   while MASTER SECRET is 48 bytes*)
          "[| evsCH: tls;  A ~= B;  Nonce NA ~: used evsCH;  NA ~: range PRF |]
           ==> Says A B {|Agent A, Nonce NA, Number SID, Number PA|}
 	        # evsCH  :  tls"
 
     ServerHello