author | wenzelm |
Mon, 24 Oct 2016 11:10:17 +0200 | |
changeset 64366 | e0ab4c0a5a93 |
parent 61830 | 4f5ab843cf5b |
child 65538 | a39ef48fbee0 |
permissions | -rw-r--r-- |
(* Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1996 University of Cambridge *) section \<open>Conventional protocols: rely on conventional Message, Event and Public -- Shared-key protocols\<close> 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