| author | wenzelm |
| Sun, 18 Nov 2012 16:31:41 +0100 | |
| changeset 50120 | 245f5947233c |
| parent 32632 | 8ae912371831 |
| child 58889 | 5b7a9633cfa8 |
| permissions | -rw-r--r-- |
(* Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1996 University of Cambridge *) header {* Conventional protocols: rely on conventional Message, Event and Public -- Shared-key protocols *} theory Auth_Shared imports "NS_Shared" "Kerberos_BAN" "Kerberos_BAN_Gets" "KerberosIV" "KerberosIV_Gets" "KerberosV" "OtwayRees" "OtwayRees_AN" "OtwayRees_Bad" "OtwayReesBella" "WooLam" "Recur" "Yahalom" "Yahalom2" "Yahalom_Bad" "ZhouGollmann" begin end