diff --git a/thys/ROOTS b/thys/ROOTS --- a/thys/ROOTS +++ b/thys/ROOTS @@ -1,569 +1,570 @@ ADS_Functor AI_Planning_Languages_Semantics AODV AVL-Trees AWN Abortable_Linearizable_Modules Abs_Int_ITP2012 Abstract-Hoare-Logics Abstract-Rewriting Abstract_Completeness Abstract_Soundness Adaptive_State_Counting Affine_Arithmetic Aggregation_Algebras Akra_Bazzi Algebraic_Numbers Algebraic_VCs Allen_Calculus Amicable_Numbers Amortized_Complexity AnselmGod Applicative_Lifting Approximation_Algorithms Architectural_Design_Patterns Aristotles_Assertoric_Syllogistic Arith_Prog_Rel_Primes ArrowImpossibilityGS Attack_Trees Auto2_HOL Auto2_Imperative_HOL AutoFocus-Stream Automated_Stateful_Protocol_Verification Automatic_Refinement AxiomaticCategoryTheory BDD BNF_CC BNF_Operations Banach_Steinhaus Bell_Numbers_Spivey Berlekamp_Zassenhaus Bernoulli Bertrands_Postulate Bicategory BinarySearchTree Binding_Syntax_Theory Binomial-Heaps Binomial-Queues BirdKMP Bondy Boolean_Expression_Checkers Bounded_Deducibility_Security Buchi_Complementation Budan_Fourier Buffons_Needle Buildings BytecodeLogicJmlTypes C2KA_DistributedSystems CAVA_Automata CAVA_LTL_Modelchecker CCS CISC-Kernel CRDT CYK CakeML CakeML_Codegen Call_Arity Card_Equiv_Relations Card_Multisets Card_Number_Partitions Card_Partitions Cartan_FP Case_Labeling Catalan_Numbers Category Category2 Category3 Cauchy Cayley_Hamilton Certification_Monads Chandy_Lamport Chord_Segments Circus Clean ClockSynchInst Closest_Pair_Points CofGroups Coinductive Coinductive_Languages Collections Comparison_Sort_Lower_Bound Compiling-Exceptions-Correctly Complete_Non_Orders Completeness Complex_Geometry Complx ComponentDependencies ConcurrentGC ConcurrentIMP Concurrent_Ref_Alg Concurrent_Revisions Consensus_Refined Constructive_Cryptography Constructor_Funs Containers CoreC++ Core_DOM Core_SC_DOM Count_Complex_Roots CryptHOL CryptoBasedCompositionalProperties DFS_Framework DPT-SAT-Solver DataRefinementIBP Datatype_Order_Generator Decl_Sem_Fun_PL Decreasing-Diagrams Decreasing-Diagrams-II Deep_Learning Density_Compiler Dependent_SIFUM_Refinement Dependent_SIFUM_Type_Systems Depth-First-Search Derangements Deriving Descartes_Sign_Rule Dict_Construction Differential_Dynamic_Logic Differential_Game_Logic Dijkstra_Shortest_Path Diophantine_Eqns_Lin_Hom Dirichlet_L Dirichlet_Series DiscretePricing Discrete_Summation DiskPaxos DynamicArchitectures Dynamic_Tables E_Transcendental Echelon_Form EdmondsKarp_Maxflow Efficient-Mergesort Elliptic_Curves_Group_Law Encodability_Process_Calculi Epistemic_Logic Ergodic_Theory Error_Function Euler_MacLaurin Euler_Partition Example-Submission Extended_Finite_State_Machine_Inference Extended_Finite_State_Machines FFT FLP FOL-Fitting FOL_Harrison FOL_Seq_Calc1 Factored_Transition_System_Bounding Falling_Factorial_Sum Farkas FeatherweightJava Featherweight_OCL Fermat3_4 FileRefinement FinFun Finger-Trees Finite_Automata_HF Finite-Map-Extras First_Order_Terms First_Welfare_Theorem Fishburn_Impossibility Fisher_Yates Flow_Networks Floyd_Warshall Flyspeck-Tame FocusStreamsCaseStudies Forcing Formal_SSA Formula_Derivatives Fourier Free-Boolean-Algebra Free-Groups FunWithFunctions FunWithTilings Functional-Automata Functional_Ordered_Resolution_Prover Furstenberg_Topology GPU_Kernel_PL Gabow_SCC Game_Based_Crypto Gauss-Jordan-Elim-Fun Gauss_Jordan Gauss_Sums Gaussian_Integers GenClock General-Triangle Generalized_Counting_Sort Generic_Deriving Generic_Join GewirthPGCProof Girth_Chromatic GoedelGod Goedel_HFSet_Semantic Goedel_HFSet_Semanticless Goedel_Incompleteness Goodstein_Lambda GraphMarkingIBP Graph_Saturation Graph_Theory Green Groebner_Bases Groebner_Macaulay Gromov_Hyperbolicity Group-Ring-Module HOL-CSP HOLCF-Prelude HRB-Slicing Heard_Of Hello_World HereditarilyFinite Hermite Hidden_Markov_Models Higher_Order_Terms Hoare_Time HotelKeyCards Huffman Hybrid_Logic Hybrid_Multi_Lane_Spatial_Logic Hybrid_Systems_VCs HyperCTL IEEE_Floating_Point IMAP-CRDT IMO2019 IMP2 IMP2_Binary_Heap IP_Addresses Imperative_Insertion_Sort Impossible_Geometry Incompleteness Incredible_Proof_Machine Inductive_Confidentiality Inductive_Inference InfPathElimination InformationFlowSlicing InformationFlowSlicing_Inter Integration Interval_Arithmetic_Word32 Iptables_Semantics Irrational_Series_Erdos_Straus Irrationality_J_Hancl Isabelle_C Isabelle_Marries_Dirac Isabelle_Meta_Model Jacobson_Basic_Algebra Jinja JinjaThreads JiveDataStoreModel Jordan_Hoelder Jordan_Normal_Form KAD KAT_and_DRA KBPs KD_Tree Key_Agreement_Strong_Adversaries Kleene_Algebra Knot_Theory Knuth_Bendix_Order Knuth_Morris_Pratt Koenigsberg_Friendship Kruskal Kuratowski_Closure_Complement LLL_Basis_Reduction LLL_Factorization LOFT LTL LTL_Master_Theorem LTL_Normal_Form LTL_to_DRA LTL_to_GBA Lam-ml-Normalization LambdaAuth LambdaMu Lambda_Free_EPO Lambda_Free_KBOs Lambda_Free_RPOs Lambert_W Landau_Symbols Laplace_Transform Latin_Square LatticeProperties Launchbury Lazy-Lists-II Lazy_Case Lehmer Lifting_Definition_Option LightweightJava LinearQuantifierElim Linear_Inequalities Linear_Programming Linear_Recurrences Liouville_Numbers List-Index List-Infinite List_Interleaving List_Inversions List_Update LocalLexing Localization_Ring Locally-Nameless-Sigma Lowe_Ontological_Argument Lower_Semicontinuous Lp Lucas_Theorem MFMC_Countable MFODL_Monitor_Optimized MFOTL_Monitor MSO_Regex_Equivalence Markov_Models Marriage Mason_Stothers Matrices_for_ODEs Matrix Matrix_Tensor Matroids Max-Card-Matching Median_Of_Medians_Selection Menger Mersenne_Primes MiniML Minimal_SSA Minkowskis_Theorem Minsky_Machines Modal_Logics_for_NTS Modular_Assembly_Kit_Security Monad_Memo_DP Monad_Normalisation MonoBoolTranAlgebra MonoidalCategory Monomorphic_Monad MuchAdoAboutTwo Multi_Party_Computation Multirelations Myhill-Nerode Name_Carrying_Type_Inference Nash_Williams Nat-Interval-Logic Native_Word Nested_Multisets_Ordinals Network_Security_Policy_Verification Neumann_Morgenstern_Utility No_FTL_observers Nominal2 Noninterference_CSP Noninterference_Concurrent_Composition Noninterference_Generic_Unwinding Noninterference_Inductive_Unwinding Noninterference_Ipurge_Unwinding Noninterference_Sequential_Composition NormByEval Nullstellensatz Octonions OpSets Open_Induction Optics Optimal_BST Orbit_Stabiliser Order_Lattice_Props Ordered_Resolution_Prover Ordinal Ordinal_Partitions Ordinals_and_Cardinals Ordinary_Differential_Equations PAC_Checker PCF PLM POPLmark-deBruijn PSemigroupsConvolution Pairing_Heap Paraconsistency Parity_Game Partial_Function_MR Partial_Order_Reduction Password_Authentication_Protocol Pell Perfect-Number-Thm Perron_Frobenius Physical_Quantities Pi_Calculus Pi_Transcendental Planarity_Certificates Poincare_Bendixson Poincare_Disc Polynomial_Factorization Polynomial_Interpolation Polynomials Pop_Refinement Posix-Lexing Possibilistic_Noninterference Power_Sum_Polynomials Pratt_Certificate Presburger-Automata Prim_Dijkstra_Simple Prime_Distribution_Elementary Prime_Harmonic_Series Prime_Number_Theorem Priority_Queue_Braun Priority_Search_Trees Probabilistic_Noninterference Probabilistic_Prime_Tests Probabilistic_System_Zoo Probabilistic_Timed_Automata Probabilistic_While Program-Conflict-Analysis Projective_Geometry Promela Proof_Strategy_Language PropResPI Propositional_Proof_Systems Prpu_Maxflow PseudoHoops Psi_Calculi Ptolemys_Theorem QHLProver QR_Decomposition Quantales Quaternions Quick_Sort_Cost RIPEMD-160-SPARK ROBDD RSAPSS Ramsey-Infinite Random_BSTs Random_Graph_Subgraph_Threshold Randomised_BSTs Randomised_Social_Choice Rank_Nullity_Theorem Real_Impl Recursion-Addition Recursion-Theory-I Refine_Imperative_HOL Refine_Monadic RefinementReactive Regex_Equivalence Regular-Sets Regular_Algebras Relation_Algebra Relational-Incorrectness-Logic Relational_Disjoint_Set_Forests +Relational_Method Relational_Paths Rep_Fin_Groups Residuated_Lattices Resolution_FOL Rewriting_Z Ribbon_Proofs Robbins-Conjecture Robinson_Arithmetic Root_Balanced_Tree Routing Roy_Floyd_Warshall SATSolverVerification SC_DOM_Components SDS_Impossibility SIFPL SIFUM_Type_Systems SPARCv8 Safe_Distance Safe_OCL Saturation_Framework Secondary_Sylow Security_Protocol_Refinement Selection_Heap_Sort SenSocialChoice Separata Separation_Algebra Separation_Logic_Imperative_HOL SequentInvertibility Shadow_SC_DOM Shivers-CFA ShortestPath Show Sigma_Commit_Crypto Signature_Groebner Simpl Simple_Firewall Simplex Skew_Heap Skip_Lists Slicing Sliding_Window_Algorithm Smith_Normal_Form Smooth_Manifolds Sort_Encodings Source_Coding_Theorem Special_Function_Bounds Splay_Tree Sqrt_Babylonian Stable_Matching Statecharts Stateful_Protocol_Composition_and_Typing Stellar_Quorums Stern_Brocot Stewart_Apollonius Stirling_Formula Stochastic_Matrices Stone_Algebras Stone_Kleene_Relation_Algebras Stone_Relation_Algebras Store_Buffer_Reduction Stream-Fusion Stream_Fusion_Code Strong_Security Sturm_Sequences Sturm_Tarski Stuttering_Equivalence Subresultants Subset_Boolean_Algebras SumSquares SuperCalc Surprise_Paradox Symmetric_Polynomials Syntax_Independent_Logic Szpilrajn TESL_Language TLA Tail_Recursive_Functions Tarskis_Geometry Taylor_Models Timed_Automata Topology TortoiseHare Transcendence_Series_Hancl_Rucki Transformer_Semantics Transition_Systems_and_Automata Transitive-Closure Transitive-Closure-II Treaps Tree-Automata Tree_Decomposition Triangle Trie Twelvefold_Way Tycon Types_Tableaus_and_Goedels_God UPF UPF_Firewall UTP Universal_Turing_Machine UpDown_Scheme Valuation VectorSpace VeriComp Verified-Prover Verified_SAT_Based_AI_Planning VerifyThis2018 VerifyThis2019 Vickrey_Clarke_Groves VolpanoSmith WHATandWHERE_Security WOOT_Strong_Eventual_Consistency WebAssembly Weight_Balanced_Trees Well_Quasi_Orders Winding_Number_Eval Word_Lib WorkerWrapper XML ZFC_in_HOL Zeta_3_Irrational Zeta_Function pGCL diff --git a/thys/Relational_Method/Anonymity.thy b/thys/Relational_Method/Anonymity.thy new file mode 100644 --- /dev/null +++ b/thys/Relational_Method/Anonymity.thy @@ -0,0 +1,591 @@ +(* Title: The Relational Method with Message Anonymity for the Verification of Cryptographic Protocols + Author: Pasquale Noce + Software Engineer at HID Global, Italy + pasquale dot noce dot lavoro at gmail dot com + pasquale dot noce at hidglobal dot com +*) + +section "Anonymity properties" + +theory Anonymity + imports Authentication +begin + +text \ +\label{Anonymity} +\ + + +proposition crypts_empty [simp]: + "crypts {} = {}" +by (rule equalityI, rule subsetI, erule crypts.induct, simp_all) + +proposition crypts_mono: + "H \ H' \ crypts H \ crypts H'" +by (rule subsetI, erule crypts.induct, auto) + +lemma crypts_union_1: + "crypts (H \ H') \ crypts H \ crypts H'" +by (rule subsetI, erule crypts.induct, auto) + +lemma crypts_union_2: + "crypts H \ crypts H' \ crypts (H \ H')" +by (rule subsetI, erule UnE, erule_tac [!] crypts.induct, auto) + +proposition crypts_union: + "crypts (H \ H') = crypts H \ crypts H'" +by (rule equalityI, rule crypts_union_1, rule crypts_union_2) + +proposition crypts_insert: + "crypts (insert X H) = crypts_msg X \ crypts H" +by (simp only: insert_def crypts_union, subst crypts_msg_def, simp) + +proposition crypts_msg_num [simp]: + "crypts_msg (Num n) = {Num n}" +by (subst crypts_msg_def, rule equalityI, rule subsetI, erule crypts.induct, simp, + rotate_tac [1-3], erule_tac [1-3] rev_mp, rule_tac [1-3] list.induct, simp_all, + blast) + +proposition crypts_msg_agent [simp]: + "crypts_msg (Agent n) = {Agent n}" +by (subst crypts_msg_def, rule equalityI, rule subsetI, erule crypts.induct, simp, + rotate_tac [1-3], erule_tac [1-3] rev_mp, rule_tac [1-3] list.induct, simp_all, + blast) + +proposition crypts_msg_pwd [simp]: + "crypts_msg (Pwd n) = {Pwd n}" +by (subst crypts_msg_def, rule equalityI, rule subsetI, erule crypts.induct, simp, + rotate_tac [1-3], erule_tac [1-3] rev_mp, rule_tac [1-3] list.induct, simp_all, + blast) + +proposition crypts_msg_key [simp]: + "crypts_msg (Key K) = {Key K}" +by (subst crypts_msg_def, rule equalityI, rule subsetI, erule crypts.induct, simp, + rotate_tac [1-3], erule_tac [1-3] rev_mp, rule_tac [1-3] list.induct, simp_all, + blast) + +proposition crypts_msg_mult [simp]: + "crypts_msg (A \ B) = {A \ B}" +by (subst crypts_msg_def, rule equalityI, rule subsetI, erule crypts.induct, simp, + rotate_tac [1-3], erule_tac [1-3] rev_mp, rule_tac [1-3] list.induct, simp_all, + blast) + +lemma crypts_hash_1: + "crypts {Hash X} \ insert (Hash X) (crypts {X})" +by (rule subsetI, erule crypts.induct, simp_all, (erule disjE, rotate_tac, erule rev_mp, + rule list.induct, simp_all, blast, (drule crypts_hash, simp)?)+) + +lemma crypts_hash_2: + "insert (Hash X) (crypts {X}) \ crypts {Hash X}" +by (rule subsetI, simp, erule disjE, blast, erule crypts.induct, simp, + subst id_apply [symmetric], subst foldr_Nil [symmetric], rule crypts_hash, simp, + blast+) + +proposition crypts_msg_hash [simp]: + "crypts_msg (Hash X) = insert (Hash X) (crypts_msg X)" +by (simp add: crypts_msg_def, rule equalityI, rule crypts_hash_1, rule crypts_hash_2) + +proposition crypts_comp: + "X \ crypts H \ Crypt K X \ crypts (Crypt K ` H)" +by (erule crypts.induct, blast, (simp only: comp_apply + [symmetric, where f = "Crypt K"] foldr_Cons [symmetric], + (erule crypts_hash | erule crypts_fst | erule crypts_snd))+) + +lemma crypts_crypt_1: + "crypts {Crypt K X} \ Crypt K ` crypts {X}" +by (rule subsetI, erule crypts.induct, simp, rotate_tac [!], erule_tac [!] rev_mp, + rule_tac [!] list.induct, auto) + +lemma crypts_crypt_2: + "Crypt K ` crypts {X} \ crypts {Crypt K X}" +by (rule subsetI, simp add: image_iff, erule bexE, drule crypts_comp, simp) + +proposition crypts_msg_crypt [simp]: + "crypts_msg (Crypt K X) = Crypt K ` crypts_msg X" +by (simp add: crypts_msg_def, rule equalityI, rule crypts_crypt_1, rule crypts_crypt_2) + +lemma crypts_mpair_1: + "crypts {\X, Y\} \ insert \X, Y\ (crypts {X} \ crypts {Y})" +by (rule subsetI, erule crypts.induct, simp_all, (erule disjE, rotate_tac, erule rev_mp, + rule list.induct, (simp+, blast)+)+) + +lemma crypts_mpair_2: + "insert \X, Y\ (crypts {X} \ crypts {Y}) \ crypts {\X, Y\}" +by (rule subsetI, simp, erule disjE, blast, erule disjE, (erule crypts.induct, simp, + subst id_apply [symmetric], subst foldr_Nil [symmetric], (rule crypts_fst [of _ X] | + rule crypts_snd), rule crypts_used, simp, blast+)+) + +proposition crypts_msg_mpair [simp]: + "crypts_msg \X, Y\ = insert \X, Y\ (crypts_msg X \ crypts_msg Y)" +by (simp add: crypts_msg_def, rule equalityI, rule crypts_mpair_1, rule crypts_mpair_2) + + +proposition foldr_crypt_size: + "size (foldr Crypt KS X) = size X + length KS" +by (induction KS, simp_all) + +proposition key_sets_empty [simp]: + "key_sets X {} = {}" +by (simp add: key_sets_def) + +proposition key_sets_mono: + "H \ H' \ key_sets X H \ key_sets X H'" +by (auto simp add: key_sets_def) + +proposition key_sets_union: + "key_sets X (H \ H') = key_sets X H \ key_sets X H'" +by (auto simp add: key_sets_def) + +proposition key_sets_insert: + "key_sets X (insert Y H) = key_sets_msg X Y \ key_sets X H" +by (simp only: insert_def key_sets_union, subst key_sets_msg_def, simp) + +proposition key_sets_msg_eq: + "key_sets_msg X X = {{}}" +by (simp add: key_sets_msg_def key_sets_def, rule equalityI, rule subsetI, simp, + erule exE, erule rev_mp, rule list.induct, simp, rule impI, erule conjE, + drule arg_cong [of _ X size], simp_all add: foldr_crypt_size) + +proposition key_sets_msg_num [simp]: + "key_sets_msg X (Num n) = (if X = Num n then {{}} else {})" +by (simp add: key_sets_msg_eq, simp add: key_sets_msg_def key_sets_def, rule impI, + rule allI, rule list.induct, simp_all) + +proposition key_sets_msg_agent [simp]: + "key_sets_msg X (Agent n) = (if X = Agent n then {{}} else {})" +by (simp add: key_sets_msg_eq, simp add: key_sets_msg_def key_sets_def, rule impI, + rule allI, rule list.induct, simp_all) + +proposition key_sets_msg_pwd [simp]: + "key_sets_msg X (Pwd n) = (if X = Pwd n then {{}} else {})" +by (simp add: key_sets_msg_eq, simp add: key_sets_msg_def key_sets_def, rule impI, + rule allI, rule list.induct, simp_all) + +proposition key_sets_msg_key [simp]: + "key_sets_msg X (Key K) = (if X = Key K then {{}} else {})" +by (simp add: key_sets_msg_eq, simp add: key_sets_msg_def key_sets_def, rule impI, + rule allI, rule list.induct, simp_all) + +proposition key_sets_msg_mult [simp]: + "key_sets_msg X (A \ B) = (if X = A \ B then {{}} else {})" +by (simp add: key_sets_msg_eq, simp add: key_sets_msg_def key_sets_def, rule impI, + rule allI, rule list.induct, simp_all) + +proposition key_sets_msg_hash [simp]: + "key_sets_msg X (Hash Y) = (if X = Hash Y then {{}} else {})" +by (simp add: key_sets_msg_eq, simp add: key_sets_msg_def key_sets_def, rule impI, + rule allI, rule list.induct, simp_all) + +lemma key_sets_crypt_1: + "X \ Crypt K Y \ + key_sets X {Crypt K Y} \ insert (InvKey K) ` key_sets X {Y}" +by (rule subsetI, simp add: key_sets_def, erule exE, rotate_tac, erule rev_mp, + rule list.induct, auto) + +lemma key_sets_crypt_2: + "insert (InvKey K) ` key_sets X {Y} \ key_sets X {Crypt K Y}" +by (rule subsetI, simp add: key_sets_def image_iff, (erule exE, erule conjE)+, + drule arg_cong [where f = "Crypt K"], simp only: comp_apply + [symmetric, of "Crypt K"] foldr_Cons [symmetric], subst conj_commute, + rule exI, rule conjI, assumption, simp) + +proposition key_sets_msg_crypt [simp]: + "key_sets_msg X (Crypt K Y) = (if X = Crypt K Y then {{}} else + insert (InvKey K) ` key_sets_msg X Y)" +by (simp add: key_sets_msg_eq, simp add: key_sets_msg_def, rule impI, + rule equalityI, erule key_sets_crypt_1 [simplified], + rule key_sets_crypt_2 [simplified]) + +proposition key_sets_msg_mpair [simp]: + "key_sets_msg X \Y, Z\ = (if X = \Y, Z\ then {{}} else {})" +by (simp add: key_sets_msg_eq, simp add: key_sets_msg_def key_sets_def, rule impI, + rule allI, rule list.induct, simp_all) + +proposition key_sets_range: + "U \ key_sets X H \ U \ range Key" +by (simp add: key_sets_def, blast) + +proposition key_sets_crypts_hash: + "key_sets (Hash X) (crypts H) \ key_sets X (crypts H)" +by (simp add: key_sets_def, blast) + +proposition key_sets_crypts_fst: + "key_sets \X, Y\ (crypts H) \ key_sets X (crypts H)" +by (simp add: key_sets_def, blast) + +proposition key_sets_crypts_snd: + "key_sets \X, Y\ (crypts H) \ key_sets Y (crypts H)" +by (simp add: key_sets_def, blast) + + +lemma log_spied_1: + "\s \ s'; + Log X \ parts (used s) \ Log X \ spied s; + Log X \ parts (used s')\ \ + Log X \ spied s'" +by (simp add: rel_def, ((erule disjE)?, ((erule exE)+)?, simp add: parts_insert, + ((subst (asm) disj_assoc [symmetric])?, erule disjE, (drule parts_dec | + drule parts_enc | drule parts_sep | drule parts_con), simp+)?)+) + +proposition log_spied [rule_format]: + "s\<^sub>0 \ s \ + Log X \ parts (used s) \ + Log X \ spied s" +by (erule rtrancl_induct, subst parts_init, simp add: Range_iff image_def, rule impI, + rule log_spied_1) + + +proposition log_dec: + "\s\<^sub>0 \ s; s' = insert (Spy, X) s \ (Spy, Crypt K X) \ s \ + (Spy, Key (InvK K)) \ s\ \ + key_sets Y (crypts {Y. Log Y = X}) \ key_sets Y (crypts (Log -` spied s))" +by (rule key_sets_mono, rule crypts_mono, rule subsetI, simp, drule parts_dec + [where Y = X], drule_tac [!] sym, simp_all, rule log_spied [simplified]) + +proposition log_sep: + "\s\<^sub>0 \ s; s' = insert (Spy, X) (insert (Spy, Y) s) \ (Spy, \X, Y\) \ s\ \ + key_sets Z (crypts {Z. Log Z = X}) \ key_sets Z (crypts (Log -` spied s)) \ + key_sets Z (crypts {Z. Log Z = Y}) \ key_sets Z (crypts (Log -` spied s))" +by (rule conjI, (rule key_sets_mono, rule crypts_mono, rule subsetI, simp, + frule parts_sep [where Z = X], drule_tac [2] parts_sep [where Z = Y], + simp_all add: parts_msg_def, blast+, drule sym, simp, + rule log_spied [simplified], assumption+)+) + + +lemma idinfo_spied_1: + "\s \ s'; + \n, X\ \ parts (used s) \ \n, X\ \ spied s; + \n, X\ \ parts (used s')\ \ + \n, X\ \ spied s'" +by (simp add: rel_def, (erule disjE, (erule exE)+, simp add: parts_insert, + ((subst (asm) disj_assoc [symmetric])?, erule disjE, (drule parts_dec | + drule parts_enc | drule parts_sep | drule parts_con), simp+)?)+, + auto simp add: parts_insert) + +proposition idinfo_spied [rule_format]: + "s\<^sub>0 \ s \ + \n, X\ \ parts (used s) \ + \n, X\ \ spied s" +by (erule rtrancl_induct, subst parts_init, simp add: Range_iff image_def, rule impI, + rule idinfo_spied_1) + + +proposition idinfo_dec: + "\s\<^sub>0 \ s; s' = insert (Spy, X) s \ (Spy, Crypt K X) \ s \ + (Spy, Key (InvK K)) \ s; \n, Y\ = X\ \ + \n, Y\ \ spied s" +by (drule parts_dec [where Y = "\n, Y\"], drule sym, simp, rule idinfo_spied) + +proposition idinfo_sep: + "\s\<^sub>0 \ s; s' = insert (Spy, X) (insert (Spy, Y) s) \ (Spy, \X, Y\) \ s; + \n, Z\ = X \ \n, Z\ = Y\ \ + \n, Z\ \ spied s" +by (drule parts_sep [where Z = "\n, Z\"], erule disjE, (drule sym, simp)+, + rule idinfo_spied) + + +lemma idinfo_msg_1: + assumes A: "s\<^sub>0 \ s" + shows "\s \ s'; \n, X\ \ spied s \ X \ spied s; \n, X\ \ spied s'\ \ + X \ spied s'" +by (simp add: rel_def, (erule disjE, (erule exE)+, simp, ((subst (asm) disj_assoc + [symmetric])?, erule disjE, (drule idinfo_dec [OF A] | drule idinfo_sep [OF A]), + simp+ | erule disjE, (simp add: image_iff)+, blast?)?)+) + +proposition idinfo_msg [rule_format]: + "s\<^sub>0 \ s \ + \n, X\ \ spied s \ + X \ spied s" +by (erule rtrancl_induct, simp, blast, rule impI, rule idinfo_msg_1) + + +proposition parts_agent: + "\s\<^sub>0 \ s; n \ bad_agent\ \ Agent n \ parts (used s)" +by (erule rtrancl_induct, subst parts_init, simp add: Range_iff image_def, simp + add: rel_def, ((erule disjE)?, (erule exE)+, simp add: parts_insert image_iff, + (rule ccontr, (drule parts_dec | drule parts_enc | drule parts_sep | + drule parts_con), simp+)?)+) + +lemma idinfo_init_1 [rule_format]: + assumes A: "s\<^sub>0 \ s" + shows "\s \ s'; n \ bad_id_password \ bad_id_pubkey \ bad_id_shakey; + \X. \n, X\ \ spied s\ \ + \n, X\ \ spied s'" +by (rule notI, simp add: rel_def, ((erule disjE)?, (erule exE)+, (blast | simp, + ((drule idinfo_dec [OF A] | drule idinfo_sep [OF A]), simp, blast | + (erule conjE)+, drule parts_agent [OF A], blast))?)+) + +proposition idinfo_init: + "\s\<^sub>0 \ s; n \ bad_id_password \ bad_id_pubkey \ bad_id_shakey\ \ + \n, X\ \ spied s" +by (induction arbitrary: X rule: rtrancl_induct, simp add: image_def, blast, + rule idinfo_init_1) + + +lemma idinfo_mpair_1 [rule_format]: + "\(s, s') \ rel_id_hash \ rel_id_crypt \ rel_id_sep \ rel_id_con; + \X Y. \n, \X, Y\\ \ spied s \ + key_sets \X, Y\ (crypts (Log -` spied s)) \ {}; + \n, \X, Y\\ \ spied s'\ \ + key_sets \X, Y\ (crypts (Log -` spied s')) \ {}" +by ((erule disjE)?, clarify?, simp add: image_iff Image_def, (drule subsetD + [OF key_sets_crypts_hash] | drule key_sets_range, blast | (drule spec)+, + drule mp, simp, simp add: ex_in_conv [symmetric], erule exE, frule subsetD + [OF key_sets_crypts_fst], drule subsetD [OF key_sets_crypts_snd])?)+ + +lemma idinfo_mpair_2 [rule_format]: + assumes A: "s\<^sub>0 \ s" + shows "\s \ s'; (s, s') \ rel_id_hash \ rel_id_crypt \ rel_id_sep \ rel_id_con; + \X Y. \n, \X, Y\\ \ spied s \ + key_sets \X, Y\ (crypts (Log -` spied s)) \ {}; + \n, \X, Y\\ \ spied s'\ \ + key_sets \X, Y\ (crypts (Log -` spied s')) \ {}" +by (simp only: rel_def Un_iff de_Morgan_disj, simp, ((erule disjE)?, (erule exE)+, + simp add: Image_def, (simp only: Collect_disj_eq crypts_union key_sets_union, simp)?, + ((subst (asm) disj_assoc [symmetric])?, erule disjE, (drule idinfo_dec [OF A] | + drule idinfo_sep [OF A]), simp+)?)+) + +proposition idinfo_mpair [rule_format]: + "s\<^sub>0 \ s \ + \n, \X, Y\\ \ spied s \ + key_sets \X, Y\ (crypts (Log -` spied s)) \ {}" +proof (induction arbitrary: X Y rule: rtrancl_induct, simp add: image_def, + rule impI) + fix s s' X Y + assume + "s\<^sub>0 \ s" and + "s \ s'" and + "\X Y. \n, \X, Y\\ \ spied s \ + key_sets \X, Y\ (crypts (Log -` spied s)) \ {}" and + "\n, \X, Y\\ \ spied s'" + thus "key_sets \X, Y\ (crypts (Log -` spied s')) \ {}" + by (cases "(s, s') \ rel_id_hash \ rel_id_crypt \ rel_id_sep \ rel_id_con", + erule_tac [2] idinfo_mpair_2, erule_tac idinfo_mpair_1, simp_all) +qed + + +proposition key_sets_pwd_empty: + "s\<^sub>0 \ s \ + key_sets (Hash (Pwd n)) (crypts (Log -` spied s)) = {} \ + key_sets \Pwd n, X\ (crypts (Log -` spied s)) = {} \ + key_sets \X, Pwd n\ (crypts (Log -` spied s)) = {}" + (is "_ \ key_sets ?X (?H s) = _ \ key_sets ?Y _ = _ \ key_sets ?Z _ = _") +proof (erule rtrancl_induct, simp add: image_iff Image_def) + fix s s' + assume + A: "s\<^sub>0 \ s" and + B: "s \ s'" and + C: "key_sets (Hash (Pwd n)) (?H s) = {} \ + key_sets \Pwd n, X\ (?H s) = {} \ + key_sets \X, Pwd n\ (?H s) = {}" + show "key_sets (Hash (Pwd n)) (?H s') = {} \ + key_sets \Pwd n, X\ (?H s') = {} \ + key_sets \X, Pwd n\ (?H s') = {}" + by (insert B C, simp add: rel_def, ((erule disjE)?, ((erule exE)+)?, simp add: + image_iff Image_def, (simp only: Collect_disj_eq crypts_union + key_sets_union, simp add: crypts_insert key_sets_insert)?, + (frule log_dec [OF A, where Y = "?X"], + frule log_dec [OF A, where Y = "?Y"], drule log_dec [OF A, where Y = "?Z"] | + frule log_sep [OF A, where Z = "?X"], frule log_sep [OF A, where Z = "?Y"], + drule log_sep [OF A, where Z = "?Z"])?)+) +qed + +proposition key_sets_pwd_seskey [rule_format]: + "s\<^sub>0 \ s \ + U \ key_sets (Pwd n) (crypts (Log -` spied s)) \ + (\SK. U = {SesKey SK} \ + ((Owner n, Crypt (SesK SK) (Pwd n)) \ s \ + (Asset n, Crypt (SesK SK) (Num 0)) \ s))" + (is "_ \ _ \ ?P s") +proof (erule rtrancl_induct, simp add: image_iff Image_def, rule impI) + fix s s' + assume + A: "s\<^sub>0 \ s" and + B: "s \ s'" and + C: "U \ key_sets (Pwd n) (crypts (Log -` spied s)) \ ?P s" and + D: "U \ key_sets (Pwd n) (crypts (Log -` spied s'))" + show "?P s'" + by (insert B C D, simp add: rel_def, ((erule disjE)?, ((erule exE)+)?, simp + add: image_iff Image_def, (simp only: Collect_disj_eq crypts_union + key_sets_union, simp add: crypts_insert key_sets_insert split: if_split_asm, + blast?)?, (erule disjE, (drule log_dec [OF A] | drule log_sep [OF A]), + (erule conjE)?, drule subsetD, simp)?)+) +qed + + +lemma pwd_anonymous_1 [rule_format]: + "\s\<^sub>0 \ s; n \ bad_id_password\ \ + \n, Pwd n\ \ spied s \ + (\SK. SesKey SK \ spied s \ + ((Owner n, Crypt (SesK SK) (Pwd n)) \ s \ + (Asset n, Crypt (SesK SK) (Num 0)) \ s))" + (is "\_; _\ \ _ \ ?P s") +proof (erule rtrancl_induct, simp add: image_def, rule impI) + fix s s' + assume + A: "s\<^sub>0 \ s" and + B: "s \ s'" and + C: "\n, Pwd n\ \ spied s \ ?P s" and + D: "\n, Pwd n\ \ spied s'" + show "?P s'" + by (insert B C D, simp add: rel_def, ((erule disjE)?, (erule exE)+, simp add: + image_iff, blast?, ((subst (asm) disj_assoc [symmetric])?, erule disjE, + (drule idinfo_dec [OF A] | drule idinfo_sep [OF A]), simp, blast+ | + insert key_sets_pwd_empty [OF A], clarsimp)?, (((erule disjE)?, erule + conjE, drule sym, simp, (drule key_sets_pwd_seskey [OF A] | drule + idinfo_mpair [OF A, simplified]), simp)+ | drule key_sets_range, blast)?)+) +qed + +theorem pwd_anonymous: + assumes + A: "s\<^sub>0 \ s" and + B: "n \ bad_id_password" and + C: "n \ bad_shakey \ (bad_pwd \ bad_prikey) \ (bad_id_pubkey \ bad_id_shak)" + shows "\n, Pwd n\ \ spied s" +proof + assume D: "\n, Pwd n\ \ spied s" + hence "n \ bad_id_password \ bad_id_pubkey \ bad_id_shakey" + by (rule contrapos_pp, rule_tac idinfo_init [OF A]) + moreover have "\SK. SesKey SK \ spied s \ + ((Owner n, Crypt (SesK SK) (Pwd n)) \ s \ + (Asset n, Crypt (SesK SK) (Num 0)) \ s)" + (is "\SK. ?P SK \ (?Q SK \ ?R SK)") + by (rule pwd_anonymous_1 [OF A B D]) + then obtain SK where "?P SK" and "?Q SK \ ?R SK" by blast + moreover { + assume "?Q SK" + hence "n \ bad_shakey \ bad_prikey" + by (rule_tac contrapos_pp [OF `?P SK`], rule_tac owner_seskey_secret [OF A]) + } + moreover { + assume "?R SK" + hence "n \ bad_shakey \ (bad_pwd \ bad_prikey)" + by (rule_tac contrapos_pp [OF `?P SK`], rule_tac asset_seskey_secret [OF A]) + } + ultimately show False + using B and C by blast +qed + + +proposition idinfo_pwd_start: + assumes + A: "s\<^sub>0 \ s" and + B: "n \ bad_agent" + shows "\s \ s'; \X. \n, X\ \ spied s' \ X \ Pwd n; + \ (\X. \n, X\ \ spied s \ X \ Pwd n)\ \ + \SK. SesKey SK \ spied s \ + ((Owner n, Crypt (SesK SK) (Pwd n)) \ s \ + (Asset n, Crypt (SesK SK) (Num 0)) \ s)" +proof (simp add: rel_def, insert parts_agent [OF A B], insert key_sets_pwd_empty + [OF A], (erule disjE, (erule exE)+, simp, erule conjE, (subst (asm) disj_assoc + [symmetric])?, (erule disjE)?, (drule idinfo_dec [OF A] | drule idinfo_sep + [OF A] | drule spec, drule mp), simp+)+, auto, rule FalseE, rule_tac [3] FalseE) + fix X U K + assume "\X. (Spy, \n, X\) \ s \ X = Pwd n" and "(Spy, \n, K\) \ s" + hence "K = Pwd n" by simp + moreover assume "U \ key_sets X (crypts (Log -` spied s))" + hence "U \ range Key" + by (rule key_sets_range) + moreover assume "K \ U" + ultimately show False by blast +next + fix X U + assume "\X. (Spy, \n, X\) \ s \ X = Pwd n" and "(Spy, \n, X\) \ s" + hence C: "X = Pwd n" by simp + moreover assume "U \ key_sets X (crypts (Log -` spied s))" + ultimately have "U \ key_sets (Pwd n) (crypts (Log -` spied s))" by simp + hence "\SK. U = {SesKey SK} \ + ((Owner n, Crypt (SesK SK) (Pwd n)) \ s \ + (Asset n, Crypt (SesK SK) (Num 0)) \ s)" + by (rule key_sets_pwd_seskey [OF A]) + moreover assume "U \ spied s" + ultimately show "\x U V. (Spy, Key (SesK (x, U, V))) \ s \ + ((Owner n, Crypt (SesK (x, U, V)) X) \ s \ + (Asset n, Crypt (SesK (x, U, V)) (Num 0)) \ s)" + using C by auto +next + fix X U K + assume "\X. (Spy, \n, X\) \ s \ X = Pwd n" and "(Spy, \n, K\) \ s" + hence "K = Pwd n" by simp + moreover assume "U \ key_sets X (crypts (Log -` spied s))" + hence "U \ range Key" + by (rule key_sets_range) + moreover assume "K \ U" + ultimately show False by blast +qed + +proposition idinfo_pwd: + "\s\<^sub>0 \ s; \X. \n, X\ \ spied s \ X \ Pwd n; + n \ bad_id_pubkey \ bad_id_shakey\ \ + \SK. SesKey SK \ spied s \ + ((Owner n, Crypt (SesK SK) (Pwd n)) \ s \ + (Asset n, Crypt (SesK SK) (Num 0)) \ s)" +by (drule rtrancl_start, assumption, simp, blast, (erule exE)+, (erule conjE)+, + frule idinfo_pwd_start [of _ n], simp+, drule r_into_rtrancl, drule rtrancl_trans, + assumption, (drule state_subset)+, blast) + + +theorem auth_prikey_anonymous: + assumes + A: "s\<^sub>0 \ s" and + B: "n \ bad_id_prikey" and + C: "n \ bad_shakey \ bad_prikey \ (bad_id_password \ bad_id_shak)" + shows "\n, Auth_PriKey n\ \ spied s" +proof + assume D: "\n, Auth_PriKey n\ \ spied s" + hence "n \ bad_id_password \ bad_id_pubkey \ bad_id_shakey" + by (rule contrapos_pp, rule_tac idinfo_init [OF A]) + moreover have "Auth_PriKey n \ spied s" + by (rule idinfo_msg [OF A D]) + hence "n \ bad_prikey" + by (rule contrapos_pp, rule_tac auth_prikey_secret [OF A]) + moreover from this have E: "n \ bad_id_pubkey" + using B by simp + moreover have "n \ bad_shakey" + proof (cases "n \ bad_id_shakey", simp) + case False + with D and E have "\SK. SesKey SK \ spied s \ + ((Owner n, Crypt (SesK SK) (Pwd n)) \ s \ + (Asset n, Crypt (SesK SK) (Num 0)) \ s)" + (is "\SK. ?P SK \ (?Q SK \ ?R SK)") + by (rule_tac idinfo_pwd [OF A], rule_tac exI [of _ "Auth_PriKey n"], simp_all) + then obtain SK where "?P SK" and "?Q SK \ ?R SK" by blast + moreover { + assume "?Q SK" + hence "n \ bad_shakey \ bad_prikey" + by (rule_tac contrapos_pp [OF `?P SK`], rule_tac owner_seskey_secret + [OF A]) + } + moreover { + assume "?R SK" + hence "n \ bad_shakey \ (bad_pwd \ bad_prikey)" + by (rule_tac contrapos_pp [OF `?P SK`], rule_tac asset_seskey_secret + [OF A]) + } + ultimately show ?thesis by blast + qed + ultimately show False + using C by blast +qed + + +theorem auth_shakey_anonymous: + assumes + A: "s\<^sub>0 \ s" and + B: "n \ bad_id_shakey" and + C: "n \ bad_shakey \ (bad_id_password \ bad_id_pubkey)" + shows "\n, Key (Auth_ShaKey n)\ \ spied s" +proof + assume D: "\n, Key (Auth_ShaKey n)\ \ spied s" + hence "n \ bad_id_password \ bad_id_pubkey \ bad_id_shakey" + by (rule contrapos_pp, rule_tac idinfo_init [OF A]) + moreover have "Key (Auth_ShaKey n) \ spied s" + by (rule idinfo_msg [OF A D]) + hence "n \ bad_shakey" + by (rule contrapos_pp, rule_tac auth_shakey_secret [OF A]) + ultimately show False + using B and C by blast +qed + + +end diff --git a/thys/Relational_Method/Authentication.thy b/thys/Relational_Method/Authentication.thy new file mode 100644 --- /dev/null +++ b/thys/Relational_Method/Authentication.thy @@ -0,0 +1,1903 @@ +(* Title: The Relational Method with Message Anonymity for the Verification of Cryptographic Protocols + Author: Pasquale Noce + Software Engineer at HID Global, Italy + pasquale dot noce dot lavoro at gmail dot com + pasquale dot noce at hidglobal dot com +*) + +section "Confidentiality and authenticity properties" + +theory Authentication + imports Definitions +begin + +text \ +\label{Authentication} +\ + + +proposition rtrancl_start [rule_format]: + "(x, y) \ r\<^sup>* \ P y \ \ P x \ + (\u v. (x, u) \ r\<^sup>* \ (u, v) \ r \ (v, y) \ r\<^sup>* \ \ P u \ P v)" + (is "_ \ _ \ _ \ (\u v. ?Q x y u v)") +proof (erule rtrancl_induct, simp, (rule impI)+) + fix y z + assume + A: "(x, y) \ r\<^sup>*" and + B: "(y, z) \ r" and + C: "P z" + assume "P y \ \ P x \(\u v. ?Q x y u v)" and "\ P x" + hence D: "P y \ (\u v. ?Q x y u v)" by simp + show "\u v. ?Q x z u v" + proof (cases "P y") + case True + with D obtain u v where "?Q x y u v" by blast + moreover from this and B have "(v, z) \ r\<^sup>*" by auto + ultimately show ?thesis by blast + next + case False + with A and B and C have "?Q x z y z" by simp + thus ?thesis by blast + qed +qed + + +proposition state_subset: + "s \ s' \ s \ s'" +by (erule rtrancl_induct, auto simp add: rel_def image_def) + +proposition spied_subset: + "s \ s' \ spied s \ spied s'" +by (rule Image_mono, erule state_subset, simp) + +proposition used_subset: + "s \ s' \ used s \ used s'" +by (rule Range_mono, rule state_subset) + +proposition asset_ii_init: + "\s\<^sub>0 \ s; (Asset n, \Num 2, PubKey A\) \ s\ \ + PriKey A \ spied s\<^sub>0" +by (drule rtrancl_start, assumption, simp add: image_def, (erule exE)+, + erule conjE, rule notI, drule spied_subset, drule subsetD, assumption, + auto simp add: rel_def) + +proposition auth_prikey_used: + "s\<^sub>0 \ s \ Auth_PriKey n \ used s" +by (drule used_subset, erule subsetD, simp add: Range_iff image_def, blast) + +proposition asset_i_used: + "s\<^sub>0 \ s \ + (Asset n, Crypt (Auth_ShaKey n) (PriKey A)) \ s \ + PriKey A \ used s" +by (erule rtrancl_induct, auto simp add: rel_def image_def) + +proposition owner_ii_used: + "s\<^sub>0 \ s \ + (Owner n, \Num 1, PubKey A\) \ s \ + PriKey A \ used s" +by (erule rtrancl_induct, auto simp add: rel_def image_def) + +proposition asset_ii_used: + "s\<^sub>0 \ s \ + (Asset n, \Num 2, PubKey A\) \ s \ + PriKey A \ used s" +by (erule rtrancl_induct, auto simp add: rel_def image_def) + +proposition owner_iii_used: + "s\<^sub>0 \ s \ + (Owner n, \Num 3, PubKey A\) \ s \ + PriKey A \ used s" +by (erule rtrancl_induct, auto simp add: rel_def image_def) + +proposition asset_iii_used: + "s\<^sub>0 \ s \ + (Asset n, \Num 4, PubKey A\) \ s \ + PriKey A \ used s" +by (erule rtrancl_induct, auto simp add: rel_def image_def) + +proposition asset_i_unique [rule_format]: + "s\<^sub>0 \ s \ + (Asset m, Crypt (Auth_ShaKey m) (PriKey A)) \ s \ + (Asset n, Crypt (Auth_ShaKey n) (PriKey A)) \ s \ + m = n" +by (erule rtrancl_induct, simp add: image_def, frule asset_i_used [of _ m A], + drule asset_i_used [of _ n A], auto simp add: rel_def) + +proposition owner_ii_unique [rule_format]: + "s\<^sub>0 \ s \ + (Owner m, \Num 1, PubKey A\) \ s \ + (Owner n, \Num 1, PubKey A\) \ s \ + m = n" +by (erule rtrancl_induct, simp add: image_def, frule owner_ii_used [of _ m A], + drule owner_ii_used [of _ n A], auto simp add: rel_def) + +proposition asset_ii_unique [rule_format]: + "s\<^sub>0 \ s \ + (Asset m, \Num 2, PubKey A\) \ s \ + (Asset n, \Num 2, PubKey A\) \ s \ + m = n" +by (erule rtrancl_induct, simp add: image_def, frule asset_ii_used [of _ m A], + drule asset_ii_used [of _ n A], auto simp add: rel_def) + +proposition auth_prikey_asset_i [rule_format]: + "s\<^sub>0 \ s \ + (Asset m, Crypt (Auth_ShaKey m) (Auth_PriKey n)) \ s \ + False" +by (erule rtrancl_induct, simp add: image_def, drule auth_prikey_used [of _ n], + auto simp add: rel_def) + +proposition auth_pubkey_owner_ii [rule_format]: + "s\<^sub>0 \ s \ + (Owner m, \Num 1, Auth_PubKey n\) \ s \ + False" +by (erule rtrancl_induct, simp add: image_def, drule auth_prikey_used [of _ n], + auto simp add: rel_def) + +proposition auth_pubkey_asset_ii [rule_format]: + "s\<^sub>0 \ s \ + (Asset m, \Num 2, Auth_PubKey n\) \ s \ + False" +by (erule rtrancl_induct, simp add: image_def, drule auth_prikey_used [of _ n], + auto simp add: rel_def) + +proposition asset_i_owner_ii [rule_format]: + "s\<^sub>0 \ s \ + (Asset m, Crypt (Auth_ShaKey m) (PriKey A)) \ s \ + (Owner n, \Num 1, PubKey A\) \ s \ + False" +by (erule rtrancl_induct, simp add: image_def, frule asset_i_used [of _ m A], + drule owner_ii_used [of _ n A], auto simp add: rel_def) + +proposition asset_i_asset_ii [rule_format]: + "s\<^sub>0 \ s \ + (Asset m, Crypt (Auth_ShaKey m) (PriKey A)) \ s \ + (Asset n, \Num 2, PubKey A\) \ s \ + False" +by (erule rtrancl_induct, simp add: image_def, frule asset_i_used [of _ m A], + drule asset_ii_used [of _ n A], auto simp add: rel_def) + +proposition asset_ii_owner_ii [rule_format]: + "s\<^sub>0 \ s \ + (Asset m, \Num 2, PubKey A\) \ s \ + (Owner n, \Num 1, PubKey A\) \ s \ + False" +by (erule rtrancl_induct, simp add: image_def, frule asset_ii_used [of _ m A], + drule owner_ii_used [of _ n A], auto simp add: rel_def) + +proposition asset_iii_owner_iii [rule_format]: + "s\<^sub>0 \ s \ + (Asset m, \Num 4, PubKey A\) \ s \ + (Owner n, \Num 3, PubKey A\) \ s \ + False" +by (erule rtrancl_induct, simp add: image_def, frule asset_iii_used [of _ m A], + drule owner_iii_used [of _ n A], auto simp add: rel_def) + +proposition asset_iv_state [rule_format]: + "s\<^sub>0 \ s \ + (Asset n, Token n (Auth_PriK n) B C SK) \ s \ + (\A D. fst (snd SK) = {A, B} \ snd (snd SK) = {C, D} \ + (Asset n, \Num 2, PubKey B\) \ s \ (Asset n, \Num 4, PubKey D\) \ s \ + Crypt (SesK SK) (PubKey D) \ used s \ (Asset n, PubKey B) \ s)" +by (erule rtrancl_induct, auto simp add: rel_def) + +proposition owner_v_state [rule_format]: + "s\<^sub>0 \ s \ + (Owner n, Crypt (SesK SK) (Pwd n)) \ s \ + (Owner n, SesKey SK) \ s \ + (\A B C. Token n A B C SK \ used s \ B \ fst (snd SK))" +by (erule rtrancl_induct, auto simp add: rel_def, blast) + +proposition asset_v_state [rule_format]: + "s\<^sub>0 \ s \ + (Asset n, Crypt (SesK SK) (Num 0)) \ s \ + (Asset n, SesKey SK) \ s \ Crypt (SesK SK) (Pwd n) \ used s" +by (erule rtrancl_induct, simp_all add: rel_def image_def, + ((erule disjE)?, (erule exE)+, simp add: Range_Un_eq)+) + +lemma owner_seskey_nonce_1: + "\s \ s'; + (Owner n, SesKey SK) \ s \ + (\S. fst SK = Some S \ Crypt (Auth_ShaKey n) (PriKey S) \ used s) \ + fst SK = None; + (Owner n, SesKey SK) \ s'\ \ + (\S. fst SK = Some S \ Crypt (Auth_ShaKey n) (PriKey S) \ used s') \ + fst SK = None" +by (simp add: rel_def, (erule disjE, (erule exE)+, simp+)+, + split if_split_asm, auto) + +proposition owner_seskey_nonce [rule_format]: + "s\<^sub>0 \ s \ + (Owner n, SesKey SK) \ s \ + (\S. fst SK = Some S \ Crypt (Auth_ShaKey n) (PriKey S) \ used s) \ + fst SK = None" +by (erule rtrancl_induct, simp add: image_def, rule impI, rule owner_seskey_nonce_1) + +proposition owner_seskey_other [rule_format]: + "s\<^sub>0 \ s \ + (Owner n, SesKey SK) \ s \ + (\A B C D. fst (snd SK) = {A, B} \ snd (snd SK) = {C, D} \ + (Owner n, \Num 1, PubKey A\) \ s \ + (Owner n, \Num 3, PubKey C\) \ s \ + (Owner n, Crypt (SesK SK) (PubKey D)) \ s)" +by (erule rtrancl_induct, auto simp add: rel_def, blast+) + +proposition asset_seskey_nonce [rule_format]: + "s\<^sub>0 \ s \ + (Asset n, SesKey SK) \ s \ + (\S. fst SK = Some S \ (Asset n, Crypt (Auth_ShaKey n) (PriKey S)) \ s)" +by (erule rtrancl_induct, auto simp add: rel_def) + +proposition asset_seskey_other [rule_format]: + "s\<^sub>0 \ s \ + (Asset n, SesKey SK) \ s \ + (\A B C D. fst (snd SK) = {A, B} \ snd (snd SK) = {C, D} \ + (Asset n, \Num 2, PubKey B\) \ s \ (Asset n, \Num 4, PubKey D\) \ s \ + (Asset n, Token n (Auth_PriK n) B C SK) \ s)" +by (erule rtrancl_induct, auto simp add: rel_def, blast) + + +declare Range_Un_eq [simp] + +proposition used_prod [simp]: + "A \ {} \ used (A \ H) = H" +by (simp add: Range_snd) + +proposition parts_idem [simp]: + "parts (parts H) = parts H" +by (rule equalityI, rule subsetI, erule parts.induct, auto) + +proposition parts_mono: + "H \ H' \ parts H \ parts H'" +by (rule subsetI, erule parts.induct, auto) + +proposition parts_msg_mono: + "X \ H \ parts_msg X \ parts H" +by (subgoal_tac "{X} \ H", subst parts_msg_def, erule parts_mono, simp) + +lemma parts_union_1: + "parts (H \ H') \ parts H \ parts H'" +by (rule subsetI, erule parts.induct, auto) + +lemma parts_union_2: + "parts H \ parts H' \ parts (H \ H')" +by (rule subsetI, erule UnE, erule_tac [!] parts.induct, auto) + +proposition parts_union [simp]: + "parts (H \ H') = parts H \ parts H'" +by (rule equalityI, rule parts_union_1, rule parts_union_2) + +proposition parts_insert: + "parts (insert X H) = parts_msg X \ parts H" +by (simp only: insert_def parts_union, subst parts_msg_def, simp) + +proposition parts_msg_num [simp]: + "parts_msg (Num n) = {Num n}" +by (subst parts_msg_def, rule equalityI, rule subsetI, erule parts.induct, auto) + +proposition parts_msg_pwd [simp]: + "parts_msg (Pwd n) = {Pwd n}" +by (subst parts_msg_def, rule equalityI, rule subsetI, erule parts.induct, auto) + +proposition parts_msg_key [simp]: + "parts_msg (Key K) = {Key K}" +by (subst parts_msg_def, rule equalityI, rule subsetI, erule parts.induct, auto) + +proposition parts_msg_mult [simp]: + "parts_msg (A \ B) = {A \ B}" +by (subst parts_msg_def, rule equalityI, rule subsetI, erule parts.induct, auto) + +proposition parts_msg_hash [simp]: + "parts_msg (Hash X) = {Hash X}" +by (subst parts_msg_def, rule equalityI, rule subsetI, erule parts.induct, auto) + +lemma parts_crypt_1: + "parts {Crypt K X} \ insert (Crypt K X) (parts {X})" +by (rule subsetI, erule parts.induct, auto) + +lemma parts_crypt_2: + "insert (Crypt K X) (parts {X}) \ parts {Crypt K X}" +by (rule subsetI, simp, erule disjE, blast, erule parts.induct, auto) + +proposition parts_msg_crypt [simp]: + "parts_msg (Crypt K X) = insert (Crypt K X) (parts_msg X)" +by (simp add: parts_msg_def, rule equalityI, rule parts_crypt_1, rule parts_crypt_2) + +lemma parts_mpair_1: + "parts {\X, Y\} \ insert \X, Y\ (parts {X} \ parts {Y})" +by (rule subsetI, erule parts.induct, auto) + +lemma parts_mpair_2: + "insert \X, Y\ (parts {X} \ parts {Y}) \ parts {\X, Y\}" +by (rule subsetI, simp, erule disjE, blast, erule disjE, erule_tac [!] parts.induct, + auto) + +proposition parts_msg_mpair [simp]: + "parts_msg \X, Y\ = insert \X, Y\ (parts_msg X \ parts_msg Y)" +by (simp add: parts_msg_def, rule equalityI, rule parts_mpair_1, rule parts_mpair_2) + +proposition parts_msg_idinfo [simp]: + "parts_msg \n, X\ = {\n, X\}" +by (subst parts_msg_def, rule equalityI, rule subsetI, erule parts.induct, auto) + +proposition parts_msg_trace [simp]: + "parts_msg (Log X) = {Log X}" +by (subst parts_msg_def, rule equalityI, rule subsetI, erule parts.induct, auto) + +proposition parts_idinfo [simp]: + "parts (IDInfo n ` H) = IDInfo n ` H" +by (rule equalityI, rule subsetI, erule parts.induct, auto) + +proposition parts_trace [simp]: + "parts (Log ` H) = Log ` H" +by (rule equalityI, rule subsetI, erule parts.induct, auto) + +proposition parts_dec: + "\s' = insert (Spy, X) s \ (Spy, Crypt K X) \ s \ (Spy, Key (InvK K)) \ s; + Y \ parts_msg X\ \ + Y \ parts (used s)" +by (subgoal_tac "X \ parts (used s)", drule parts_msg_mono [of X], auto) + +proposition parts_enc: + "\s' = insert (Spy, Crypt K X) s \ (Spy, X) \ s \ (Spy, Key K) \ s; + Y \ parts_msg X\ \ + Y \ parts (used s)" +by (subgoal_tac "X \ parts (used s)", drule parts_msg_mono [of X], auto) + +proposition parts_sep: + "\s' = insert (Spy, X) (insert (Spy, Y) s) \ (Spy, \X, Y\) \ s; + Z \ parts_msg X \ Z \ parts_msg Y\ \ + Z \ parts (used s)" +by (erule disjE, subgoal_tac "X \ parts (used s)", drule parts_msg_mono [of X], + subgoal_tac [3] "Y \ parts (used s)", drule_tac [3] parts_msg_mono [of Y], auto) + +proposition parts_con: + "\s' = insert (Spy, \X, Y\) s \ (Spy, X) \ s \ (Spy, Y) \ s; + Z \ parts_msg X \ Z \ parts_msg Y\ \ + Z \ parts (used s)" +by (erule disjE, subgoal_tac "X \ parts (used s)", drule parts_msg_mono [of X], + subgoal_tac [3] "Y \ parts (used s)", drule_tac [3] parts_msg_mono [of Y], auto) + +lemma parts_init_1: + "parts (used s\<^sub>0) \ used s\<^sub>0 \ range (Hash \ Agent) \ + range (Hash \ Auth_PubKey) \ + range (\n. \Hash (Agent n), Hash (Auth_PubKey n)\)" +by (rule subsetI, erule parts.induct, (clarify | simp add: Range_iff image_def)+) + +lemma parts_init_2: + "used s\<^sub>0 \ range (Hash \ Agent) \ range (Hash \ Auth_PubKey) \ + range (\n. \Hash (Agent n), Hash (Auth_PubKey n)\) \ parts (used s\<^sub>0)" +by (rule subsetI, auto simp add: parts_insert) + +proposition parts_init: + "parts (used s\<^sub>0) = used s\<^sub>0 \ range (Hash \ Agent) \ + range (Hash \ Auth_PubKey) \ + range (\n. \Hash (Agent n), Hash (Auth_PubKey n)\)" +by (rule equalityI, rule parts_init_1, rule parts_init_2) + + +proposition parts_crypt_prikey_start: + "\s \ s'; Crypt K (PriKey A) \ parts (used s'); + Crypt K (PriKey A) \ parts (used s)\ \ + (\n. K = Auth_ShaKey n \ + (Asset n, Crypt (Auth_ShaKey n) (PriKey A)) \ s') \ + {PriKey A, Key K} \ spied s'" +by (simp add: rel_def, erule disjE, (erule exE)+, simp add: parts_insert, blast, + (((erule disjE)?, (erule exE)+, simp add: parts_insert image_iff)+, + ((drule parts_dec | erule disjE, simp, drule parts_enc | + drule parts_sep | drule parts_con), simp+)?)+) + +proposition parts_crypt_prikey: + "\s\<^sub>0 \ s; Crypt K (PriKey A) \ parts (used s)\ \ + (\n. K = Auth_ShaKey n \ + (Asset n, Crypt (Auth_ShaKey n) (PriKey A)) \ s) \ + {PriKey A, Key K} \ spied s" +by (drule rtrancl_start, assumption, subst parts_init, simp add: Range_iff image_def, + (erule exE)+, (erule conjE)+, frule parts_crypt_prikey_start, assumption+, + (drule state_subset)+, blast) + + +proposition parts_crypt_pubkey_start: + "\s \ s'; Crypt (SesK SK) (PubKey C) \ parts (used s'); + Crypt (SesK SK) (PubKey C) \ parts (used s)\ \ + C \ snd (snd SK) \ ((\n. (Owner n, SesKey SK) \ s') \ + (\n B. (Asset n, Token n (Auth_PriK n) B C SK) \ s')) \ + SesKey SK \ spied s'" +by (simp add: rel_def, (erule disjE, (erule exE)+, simp add: parts_insert image_iff)+, + blast, erule disjE, (erule exE)+, simp add: parts_insert image_iff, blast, + (((erule disjE)?, ((erule exE)+)?, simp add: parts_insert image_iff)+, + ((drule parts_dec | drule parts_enc | drule parts_sep | drule parts_con), simp+)?)+) + +proposition parts_crypt_pubkey: + "\s\<^sub>0 \ s; Crypt (SesK SK) (PubKey C) \ parts (used s)\ \ + C \ snd (snd SK) \ ((\n. (Owner n, SesKey SK) \ s) \ + (\n B. (Asset n, Token n (Auth_PriK n) B C SK) \ s)) \ + SesKey SK \ spied s" +by (drule rtrancl_start, assumption, subst parts_init, simp add: Range_iff image_def, + (erule exE)+, (erule conjE)+, frule parts_crypt_pubkey_start, assumption+, + (drule state_subset)+, blast) + + +proposition parts_crypt_key_start: + "\s \ s'; Crypt K (Key K') \ parts (used s'); + Crypt K (Key K') \ parts (used s); K' \ range PriK \ range PubK\ \ + {Key K', Key K} \ spied s'" +by (simp add: rel_def, (((erule disjE)?, ((erule exE)+)?, simp add: parts_insert + image_iff)+, ((drule parts_dec | drule parts_enc | drule parts_sep | drule parts_con), + simp+)?)+) + +proposition parts_crypt_key: + "\s\<^sub>0 \ s; Crypt K (Key K') \ parts (used s); + K' \ range PriK \ range PubK\ \ + {Key K', Key K} \ spied s" +by (drule rtrancl_start, assumption, subst parts_init, simp add: Range_iff image_def, + (erule exE)+, (erule conjE)+, frule parts_crypt_key_start, assumption+, + (drule state_subset)+, blast) + + +proposition parts_crypt_sign_start: + "\s \ s'; Crypt (SesK SK) (Sign n A) \ parts (used s'); + Crypt (SesK SK) (Sign n A) \ parts (used s)\ \ + (Asset n, SesKey SK) \ s' \ SesKey SK \ spied s'" +by (simp add: rel_def, (((erule disjE)?, ((erule exE)+)?, simp add: parts_insert + image_iff)+, ((drule parts_dec | drule parts_enc | drule parts_sep | drule parts_con), + simp+)?)+) + +proposition parts_crypt_sign: + "\s\<^sub>0 \ s; Crypt (SesK SK) (Sign n A) \ parts (used s)\ \ + (Asset n, SesKey SK) \ s \ SesKey SK \ spied s" +by (drule rtrancl_start, assumption, subst parts_init, simp add: Range_iff image_def, + (erule exE)+, (erule conjE)+, frule parts_crypt_sign_start, assumption+, + (drule state_subset)+, blast) + + +proposition parts_crypt_pwd_start: + "\s \ s'; Crypt K (Pwd n) \ parts (used s'); + Crypt K (Pwd n) \ parts (used s)\ \ + (\SK. K = SesK SK \ (Owner n, Crypt (SesK SK) (Pwd n)) \ s') \ + {Pwd n, Key K} \ spied s'" +by (simp add: rel_def, (((erule disjE)?, ((erule exE)+)?, simp add: parts_insert + image_iff)+, ((drule parts_dec | drule parts_enc | drule parts_sep | drule parts_con), + simp+)?)+) + +proposition parts_crypt_pwd: + "\s\<^sub>0 \ s; Crypt K (Pwd n) \ parts (used s)\ \ + (\SK. K = SesK SK \ (Owner n, Crypt (SesK SK) (Pwd n)) \ s) \ + {Pwd n, Key K} \ spied s" +by (drule rtrancl_start, assumption, subst parts_init, simp add: Range_iff image_def, + (erule exE)+, (erule conjE)+, frule parts_crypt_pwd_start, assumption+, + (drule state_subset)+, blast) + + +proposition parts_crypt_num_start: + "\s \ s'; Crypt (SesK SK) (Num 0) \ parts (used s'); + Crypt (SesK SK) (Num 0) \ parts (used s)\ \ + (\n. (Asset n, Crypt (SesK SK) (Num 0)) \ s') \ SesKey SK \ spied s'" +by (simp add: rel_def, (erule disjE, (erule exE)+, simp add: parts_insert image_iff)+, + blast, (((erule disjE)?, (erule exE)+, simp add: parts_insert image_iff)+, + ((drule parts_dec | erule disjE, simp, drule parts_enc | + drule parts_sep | drule parts_con), simp+)?)+) + +proposition parts_crypt_num: + "\s\<^sub>0 \ s; Crypt (SesK SK) (Num 0) \ parts (used s)\ \ + (\n. (Asset n, Crypt (SesK SK) (Num 0)) \ s) \ SesKey SK \ spied s" +by (drule rtrancl_start, assumption, subst parts_init, simp add: Range_iff image_def, + (erule exE)+, (erule conjE)+, frule parts_crypt_num_start, assumption+, + (drule state_subset)+, blast) + + +proposition parts_crypt_mult_start: + "\s \ s'; Crypt (SesK SK) (A \ B) \ parts (used s'); + Crypt (SesK SK) (A \ B) \ parts (used s)\ \ + B \ fst (snd SK) \ (\n C. (Asset n, Token n (Auth_PriK n) B C SK) \ s') \ + {A \ B, SesKey SK} \ spied s" +by (simp add: rel_def, (erule disjE, (erule exE)+, simp add: parts_insert image_iff)+, + blast, (((erule disjE)?, (erule exE)+, simp add: parts_insert image_iff)+, + ((drule parts_dec | erule disjE, simp, drule parts_enc | + drule parts_sep | drule parts_con), simp+)?)+) + +proposition parts_crypt_mult: + "\s\<^sub>0 \ s; Crypt (SesK SK) (A \ B) \ parts (used s)\ \ + B \ fst (snd SK) \ (\n C. (Asset n, Token n (Auth_PriK n) B C SK) \ s) \ + {A \ B, SesKey SK} \ spied s" +by (drule rtrancl_start, assumption, subst parts_init, simp add: Range_iff image_def, + (erule exE)+, (erule conjE)+, frule parts_crypt_mult_start, assumption+, + drule converse_rtrancl_into_rtrancl, assumption, drule state_subset [of _ s], + drule spied_subset [of _ s], blast) + + +proposition parts_mult_start: + "\s \ s'; A \ B \ parts (used s'); A \ B \ parts (used s)\ \ + (\n SK. A = Auth_PriK n \ (Asset n, \Num 2, PubKey B\) \ s' \ + Crypt (SesK SK) (A \ B) \ parts (used s')) \ + {PriKey A, PriKey B} \ spied s'" +by (simp add: rel_def, (erule disjE, (erule exE)+, simp add: parts_insert image_iff)+, + blast, (((erule disjE)?, (erule exE)+, simp add: parts_insert image_iff)+, + ((drule parts_dec | drule parts_enc | drule parts_sep | drule parts_con), simp+)?)+) + +proposition parts_mult: + "\s\<^sub>0 \ s; A \ B \ parts (used s)\ \ + (\n. A = Auth_PriK n \ (Asset n, \Num 2, PubKey B\) \ s) \ + {PriKey A, PriKey B} \ spied s" +by (drule rtrancl_start, assumption, subst parts_init, simp add: Range_iff image_def, + (erule exE)+, (erule conjE)+, frule parts_mult_start, assumption+, + (drule state_subset)+, blast) + + +proposition parts_mpair_key_start: + "\s \ s'; \X, Y\ \ parts (used s'); \X, Y\ \ parts (used s); + X = Key K \ Y = Key K \ K \ range PubK\ \ + {X, Y} \ spied s'" +by (erule disjE, simp_all add: rel_def, + (((erule disjE)?, (erule exE)+, simp add: parts_insert image_iff)+, + ((drule parts_dec | drule parts_enc | + drule parts_sep | erule disjE, simp, drule parts_con), simp+)?)+) + +proposition parts_mpair_key: + "\s\<^sub>0 \ s; \X, Y\ \ parts (used s); + X = Key K \ Y = Key K \ K \ range PubK\ \ + {X, Y} \ spied s" +by (drule rtrancl_start, assumption, subst parts_init, simp add: Range_iff image_def, + blast, (erule exE)+, (erule conjE)+, frule parts_mpair_key_start, assumption+, + (drule state_subset)+, blast) + + +proposition parts_mpair_pwd_start: + "\s \ s'; \X, Y\ \ parts (used s'); \X, Y\ \ parts (used s); + X = Pwd n \ Y = Pwd n\ \ + {X, Y} \ spied s'" +by (erule disjE, simp_all add: rel_def, + (((erule disjE)?, (erule exE)+, simp add: parts_insert image_iff)+, + ((drule parts_dec | drule parts_enc | + drule parts_sep | erule disjE, simp, drule parts_con), simp+)?)+) + +proposition parts_mpair_pwd: + "\s\<^sub>0 \ s; \X, Y\ \ parts (used s); X = Pwd n \ Y = Pwd n\ \ + {X, Y} \ spied s" +by (drule rtrancl_start, assumption, subst parts_init, simp add: Range_iff image_def, + blast, (erule exE)+, (erule conjE)+, frule parts_mpair_pwd_start, assumption+, + (drule state_subset)+, blast) + + +proposition parts_pubkey_false_start: + assumes + A: "s\<^sub>0 \ s" and + B: "s \ s'" and + C: "Crypt (SesK SK) (PubKey C) \ parts (used s')" and + D: "Crypt (SesK SK) (PubKey C) \ parts (used s)" and + E: "\n. (Owner n, SesKey SK) \ s'" and + F: "SesKey SK \ spied s'" + shows False +proof - + have "C \ snd (snd SK) \ ((\n. (Owner n, SesKey SK) \ s') \ + (\n B. (Asset n, Token n (Auth_PriK n) B C SK) \ s')) \ + SesKey SK \ spied s'" + (is "?P C \ ((\n. ?Q n s') \ (\n B. ?R n B C s')) \ ?S s'") + by (rule parts_crypt_pubkey_start [OF B C D]) + then obtain n B where "?P C" and "?R n B C s'" + using E and F by blast + moreover have "\ ?R n B C s" + using D by blast + ultimately have "\D. Crypt (SesK SK) (PubKey D) \ used s" + (is "\D. ?U D") + using B by (auto simp add: rel_def) + then obtain D where "?U D" .. + hence "?P D \ ((\n. ?Q n s) \ (\n B. ?R n B D s)) \ ?S s" + by (rule_tac parts_crypt_pubkey [OF A], blast) + moreover have G: "s \ s'" + by (rule state_subset, insert B, simp) + have "\n. (Owner n, SesKey SK) \ s" + by (rule allI, rule notI, drule subsetD [OF G], insert E, simp) + moreover have H: "spied s \ spied s'" + by (rule Image_mono [OF G], simp) + have "SesKey SK \ spied s" + by (rule notI, drule subsetD [OF H], insert F, contradiction) + ultimately obtain n' B' where "?R n' B' D s" by blast + have "\A' D'. fst (snd SK) = {A', B'} \ snd (snd SK) = {D, D'} \ + (Asset n', \Num 2, PubKey B'\) \ s \ + (Asset n', \Num 4, PubKey D'\) \ s \ + ?U D' \ (Asset n', PubKey B') \ s" + by (rule asset_iv_state [OF A `?R n' B' D s`]) + then obtain D' where "snd (snd SK) = {D, D'}" and "?U D'" by blast + hence "Crypt (SesK SK) (PubKey C) \ parts (used s)" + using `?P C` and `?U D` by auto + thus False + using D by contradiction +qed + +proposition parts_pubkey_false: + "\s\<^sub>0 \ s; Crypt (SesK SK) (PubKey C) \ parts (used s); + \n. (Owner n, SesKey SK) \ s; SesKey SK \ spied s\ \ + False" +proof (drule rtrancl_start, assumption, subst parts_init, simp add: Range_iff image_def, + (erule exE)+, (erule conjE)+, erule parts_pubkey_false_start, assumption+, + rule allI, rule_tac [!] notI) + fix v n + assume "(Owner n, SesKey SK) \ v" and "v \ s" + hence "(Owner n, SesKey SK) \ s" + by (erule_tac rev_subsetD, rule_tac state_subset) + moreover assume "\n. (Owner n, SesKey SK) \ s" + ultimately show False by simp +next + fix v + assume "SesKey SK \ spied v" and "v \ s" + hence "SesKey SK \ spied s" + by (erule_tac rev_subsetD, rule_tac spied_subset) + moreover assume "SesKey SK \ spied s" + ultimately show False by contradiction +qed + + +proposition asset_ii_spied_start: + assumes + A: "s\<^sub>0 \ s" and + B: "s \ s'" and + C: "PriKey B \ spied s'" and + D: "PriKey B \ spied s" and + E: "(Asset n, \Num 2, PubKey B\) \ s" + shows "Auth_PriKey n \ spied s \ + (\C SK. (Asset n, Token n (Auth_PriK n) B C SK) \ s)" + (is "_ \ (\C SK. ?P n C SK s)") +proof - + have "\A. (A \ B \ spied s \ B \ A \ spied s) \ PriKey A \ spied s" + proof (insert B C D, auto simp add: rel_def, rule_tac [!] FalseE) + assume "Key (PriK B) \ used s" + moreover have "PriKey B \ used s" + by (rule asset_ii_used [OF A, THEN mp, OF E]) + ultimately show False by simp + next + fix K + assume "(Spy, Crypt K (Key (PriK B))) \ s" + hence "Crypt K (PriKey B) \ parts (used s)" by auto + hence "(\m. K = Auth_ShaKey m \ + (Asset m, Crypt (Auth_ShaKey m) (PriKey B)) \ s) \ + {PriKey B, Key K} \ spied s" + (is "(\m. _ \ ?P m) \ _") + by (rule parts_crypt_prikey [OF A]) + then obtain m where "?P m" + using D by blast + thus False + by (rule asset_i_asset_ii [OF A _ E]) + next + fix Y + assume "(Spy, \Key (PriK B), Y\) \ s" + hence "\PriKey B, Y\ \ parts (used s)" by auto + hence "{PriKey B, Y} \ spied s" + by (rule parts_mpair_key [OF A, where K = "PriK B"], simp) + thus False + using D by simp + next + fix X + assume "(Spy, \X, Key (PriK B)\) \ s" + hence "\X, PriKey B\ \ parts (used s)" by auto + hence "{X, PriKey B} \ spied s" + by (rule parts_mpair_key [OF A, where K = "PriK B"], simp add: image_def) + thus False + using D by simp + qed + then obtain A where F: "PriKey A \ spied s" and + "A \ B \ spied s \ B \ A \ spied s" + by blast + hence "A \ B \ parts (used s) \ B \ A \ parts (used s)" by blast + moreover have "B \ A \ parts (used s)" + proof + assume "B \ A \ parts (used s)" + hence "(\m. B = Auth_PriK m \ (Asset m, \Num 2, PubKey A\) \ s) \ + {PriKey B, PriKey A} \ spied s" + by (rule parts_mult [OF A]) + then obtain m where "B = Auth_PriK m" + using D by blast + hence "(Asset n, \Num 2, Auth_PubKey m\) \ s" + using E by simp + thus False + by (rule auth_pubkey_asset_ii [OF A]) + qed + ultimately have "A \ B \ parts (used s)" by simp + with A have "\u v. s\<^sub>0 \ u \ u \ v \ v \ s \ + A \ B \ parts (used u) \ A \ B \ parts (used v)" + by (rule rtrancl_start, subst parts_init, simp add: Range_iff image_def) + then obtain u v where G: "u \ v" and H: "v \ s" and + I: "A \ B \ parts (used u)" and "A \ B \ parts (used v)" + by blast + hence "(\m SK. A = Auth_PriK m \ (Asset m, \Num 2, PubKey B\) \ v \ + Crypt (SesK SK) (A \ B) \ parts (used v)) \ + {PriKey A, PriKey B} \ spied v" + by (rule_tac parts_mult_start, simp_all) + moreover have "PriKey B \ spied v" + proof + assume "PriKey B \ spied v" + hence "PriKey B \ spied s" + by (rule rev_subsetD, rule_tac spied_subset [OF H]) + thus False + using D by contradiction + qed + ultimately obtain m SK where + J: "Crypt (SesK SK) (A \ B) \ parts (used v)" and + "A = Auth_PriK m" and "(Asset m, \Num 2, PubKey B\) \ v" + by blast + moreover from this have "(Asset m, \Num 2, PubKey B\) \ s" + by (erule_tac rev_subsetD, rule_tac state_subset [OF H]) + hence "m = n" + by (rule asset_ii_unique [OF A _ E]) + ultimately have K: "Auth_PriKey n \ spied s" + using F by simp + have "Crypt (SesK SK) (A \ B) \ parts (used u)" + using I by blast + hence "B \ fst (snd SK) \ (\m C. ?P m C SK v) \ + {A \ B, SesKey SK} \ spied u" + by (rule parts_crypt_mult_start [OF G J]) + moreover have "A \ B \ spied u" + using I by blast + ultimately obtain m' C where "?P m' C SK v" by blast + hence "?P m' C SK s" + by (rule rev_subsetD, rule_tac state_subset [OF H]) + moreover from this have "\A' D. fst (snd SK) = {A', B} \ + snd (snd SK) = {C, D} \ (Asset m', \Num 2, PubKey B\) \ s \ + (Asset m', \Num 4, PubKey D\) \ s \ + Crypt (SesK SK) (PubKey D) \ used s \ (Asset m', PubKey B) \ s" + by (rule asset_iv_state [OF A]) + hence "(Asset m', \Num 2, PubKey B\) \ s" by blast + hence "m' = n" + by (rule asset_ii_unique [OF A _ E]) + ultimately show ?thesis + using K by blast +qed + +proposition asset_ii_spied: + assumes + A: "s\<^sub>0 \ s" and + B: "PriKey B \ spied s" and + C: "(Asset n, \Num 2, PubKey B\) \ s" + shows "Auth_PriKey n \ spied s \ + (\C SK. (Asset n, Token n (Auth_PriK n) B C SK) \ s)" + (is "?P s") +proof - + have "\u v. s\<^sub>0 \ u \ u \ v \ v \ s \ + (Asset n, \Num 2, PubKey B\) \ u \ (Asset n, \Num 2, PubKey B\) \ v" + using A and C by (rule rtrancl_start, auto) + then obtain u v where "v \ s" and "(Asset n, \Num 2, PubKey B\) \ u" and + D: "s\<^sub>0 \ u" and E: "u \ v" and F: "(Asset n, \Num 2, PubKey B\) \ v" + by blast + moreover from this have "PriKey B \ spied v" + by (auto simp add: rel_def) + ultimately have "\w x. v \ w \ w \ x \ x \ s \ + PriKey B \ spied w \ PriKey B \ spied x" + using B by (rule_tac rtrancl_start, simp_all) + then obtain w x where "PriKey B \ spied w" and "PriKey B \ spied x" and + G: "v \ w" and H: "w \ x" and I: "x \ s" + by blast + moreover from this have "s\<^sub>0 \ w" + using D and E by simp + moreover have "(Asset n, \Num 2, PubKey B\) \ w" + by (rule rev_subsetD [OF F], rule state_subset [OF G]) + ultimately have "?P w" + by (rule_tac asset_ii_spied_start, simp_all) + moreover have "w \ s" + using H and I by (rule_tac state_subset, simp) + ultimately show ?thesis by blast +qed + + +proposition asset_iv_unique: + assumes + A: "s\<^sub>0 \ s" and + B: "(Asset m, Token m (Auth_PriK m) B C' SK') \ s" and + C: "(Asset n, Token n (Auth_PriK n) B C SK) \ s" + (is "?P n C SK s") + shows "m = n \ C' = C \ SK' = SK" +proof (subst (2) cases_simp [of "m = n", symmetric], simp, rule conjI, rule impI, + rule ccontr) + assume D: "\ (C' = C \ SK' = SK)" and "m = n" + moreover have "\u v. s\<^sub>0 \ u \ u \ v \ v \ s \ + \ (?P m C' SK' u \ ?P n C SK u) \ ?P m C' SK' v \ ?P n C SK v" + using B and C by (rule_tac rtrancl_start [OF A], auto) + ultimately obtain u v where E: "s\<^sub>0 \ u" and F: "u \ v" and + G: "?P n C' SK' v" and H: "?P n C SK v" and + "\ ?P n C' SK' u \ \ ?P n C SK u" + by blast + moreover { + assume I: "\ ?P n C' SK' u" + hence "?P n C SK u" + by (insert D F G H, auto simp add: rel_def) + hence "\A D. fst (snd SK) = {A, B} \ snd (snd SK) = {C, D} \ + (Asset n, \Num 2, PubKey B\) \ u \ (Asset n, \Num 4, PubKey D\) \ u \ + Crypt (SesK SK) (PubKey D) \ used u \ (Asset n, PubKey B) \ u" + by (rule asset_iv_state [OF E]) + moreover have "(Asset n, PubKey B) \ u" + by (insert F G I, auto simp add: rel_def) + ultimately have False by simp + } + moreover { + assume I: "\ ?P n C SK u" + hence "?P n C' SK' u" + by (insert D F G H, auto simp add: rel_def) + hence "\A D. fst (snd SK') = {A, B} \ snd (snd SK') = {C', D} \ + (Asset n, \Num 2, PubKey B\) \ u \ (Asset n, \Num 4, PubKey D\) \ u \ + Crypt (SesK SK') (PubKey D) \ used u \ (Asset n, PubKey B) \ u" + by (rule asset_iv_state [OF E]) + moreover have "(Asset n, PubKey B) \ u" + by (insert F H I, auto simp add: rel_def) + ultimately have False by simp + } + ultimately show False by blast +next + have "\A D. fst (snd SK') = {A, B} \ snd (snd SK') = {C', D} \ + (Asset m, \Num 2, PubKey B\) \ s \ (Asset m, \Num 4, PubKey D\) \ s \ + Crypt (SesK SK') (PubKey D) \ used s \ (Asset m, PubKey B) \ s" + (is "?Q m C' SK'") + by (rule asset_iv_state [OF A B]) + hence "(Asset m, \Num 2, PubKey B\) \ s" by blast + moreover have "?Q n C SK" + by (rule asset_iv_state [OF A C]) + hence "(Asset n, \Num 2, PubKey B\) \ s" by blast + ultimately show "m = n" + by (rule asset_ii_unique [OF A]) +qed + + +theorem sigkey_secret: + "s\<^sub>0 \ s \ SigKey \ spied s" +proof (erule rtrancl_induct, simp add: image_def) + fix s s' + assume + A: "s\<^sub>0 \ s" and + B: "s \ s'" and + C: "SigKey \ spied s" + show "SigKey \ spied s'" + proof (insert B C, auto simp add: rel_def) + fix K + assume "(Spy, Crypt K SigKey) \ s" + hence "Crypt K SigKey \ parts (used s)" by blast + hence "{SigKey, Key K} \ spied s" + by (rule parts_crypt_key [OF A], simp add: image_def) + with C show False by simp + next + fix Y + assume "(Spy, \SigKey, Y\) \ s" + hence "\SigKey, Y\ \ parts (used s)" by blast + hence "{SigKey, Y} \ spied s" + by (rule parts_mpair_key [OF A, where K = "SigK"], simp) + with C show False by simp + next + fix X + assume "(Spy, \X, SigKey\) \ s" + hence "\X, SigKey\ \ parts (used s)" by blast + hence "{X, SigKey} \ spied s" + by (rule parts_mpair_key [OF A, where K = "SigK"], simp add: image_def) + with C show False by simp + qed +qed + +proposition parts_sign_start: + assumes A: "s\<^sub>0 \ s" + shows "\s \ s'; Sign n A \ parts (used s'); Sign n A \ parts (used s)\ \ + A = Auth_PriK n" +by (simp add: rel_def, (((erule disjE)?, (erule exE)+, simp add: parts_insert image_iff)+, + ((drule parts_dec | erule disjE, insert sigkey_secret [OF A], simp, drule parts_enc | + drule parts_sep | drule parts_con), simp+)?)+) + +proposition parts_sign: + "\s\<^sub>0 \ s; Sign n A \ parts (used s)\ \ + A = Auth_PriK n" +by (rule classical, drule rtrancl_start, assumption, subst parts_init, simp add: + Range_iff image_def, (erule exE)+, (erule conjE)+, drule parts_sign_start) + + +theorem auth_shakey_secret: + "\s\<^sub>0 \ s; n \ bad_shakey\ \ + Key (Auth_ShaKey n) \ spied s" +proof (erule rtrancl_induct, simp add: image_def) + fix s s' + assume + A: "s\<^sub>0 \ s" and + B: "s \ s'" and + C: "Key (Auth_ShaKey n) \ spied s" + show "Key (Auth_ShaKey n) \ spied s'" + proof (insert B C, auto simp add: rel_def) + fix K + assume "(Spy, Crypt K (Key (ShaK (Auth_ShaK n)))) \ s" + hence "Crypt K (Key (Auth_ShaKey n)) \ parts (used s)" by auto + hence "{Key (Auth_ShaKey n), Key K} \ spied s" + by (rule parts_crypt_key [OF A], simp add: image_def) + with C show False by simp + next + fix Y + assume "(Spy, \Key (ShaK (Auth_ShaK n)), Y\) \ s" + hence "\Key (Auth_ShaKey n), Y\ \ parts (used s)" by auto + hence "{Key (Auth_ShaKey n), Y} \ spied s" + by (rule parts_mpair_key [OF A, where K = "Auth_ShaKey n"], simp) + with C show False by simp + next + fix X + assume "(Spy, \X, Key (ShaK (Auth_ShaK n))\) \ s" + hence "\X, Key (Auth_ShaKey n)\ \ parts (used s)" by auto + hence "{X, Key (Auth_ShaKey n)} \ spied s" + by (rule parts_mpair_key [OF A, where K = "Auth_ShaKey n"], + simp add: image_def) + with C show False by simp + qed +qed + + +theorem auth_prikey_secret: + assumes + A: "s\<^sub>0 \ s" and + B: "n \ bad_prikey" + shows "Auth_PriKey n \ spied s" +proof + assume "Auth_PriKey n \ spied s" + moreover have "Auth_PriKey n \ spied s\<^sub>0" + using B by auto + ultimately have "\u v. s\<^sub>0 \ u \ u \ v \ v \ s \ + Auth_PriKey n \ spied u \ Auth_PriKey n \ spied v" + by (rule rtrancl_start [OF A]) + then obtain u v where C: "s\<^sub>0 \ u" and D: "u \ v" and + E: "Auth_PriKey n \ spied u" and F: "Auth_PriKey n \ spied v" + by blast + have "\B. (Auth_PriK n \ B \ spied u \ B \ Auth_PriK n \ spied u) \ + PriKey B \ spied u" + proof (insert D E F, auto simp add: rel_def, rule_tac [!] FalseE) + assume "Key (PriK (Auth_PriK n)) \ used u" + moreover have "Auth_PriKey n \ used u" + by (rule auth_prikey_used [OF C]) + ultimately show False by simp + next + fix K + assume "(Spy, Crypt K (Key (PriK (Auth_PriK n)))) \ u" + hence "Crypt K (PriKey (Auth_PriK n)) \ parts (used u)" by auto + hence "(\m. K = Auth_ShaKey m \ + (Asset m, Crypt (Auth_ShaKey m) (PriKey (Auth_PriK n))) \ u) \ + {PriKey (Auth_PriK n), Key K} \ spied u" + by (rule parts_crypt_prikey [OF C]) + then obtain m where + "(Asset m, Crypt (Auth_ShaKey m) (Auth_PriKey n)) \ u" + using E by auto + thus False + by (rule auth_prikey_asset_i [OF C]) + next + fix Y + assume "(Spy, \Key (PriK (Auth_PriK n)), Y\) \ u" + hence "\Auth_PriKey n, Y\ \ parts (used u)" by auto + hence "{Auth_PriKey n, Y} \ spied u" + by (rule parts_mpair_key [OF C, where K = "PriK (Auth_PriK n)"], simp) + thus False + using E by simp + next + fix X + assume "(Spy, \X, Key (PriK (Auth_PriK n))\) \ u" + hence "\X, Auth_PriKey n\ \ parts (used u)" by auto + hence "{X, Auth_PriKey n} \ spied u" + by (rule parts_mpair_key [OF C, where K = "PriK (Auth_PriK n)"], simp + add: image_def) + thus False + using E by simp + qed + then obtain B where G: "PriKey B \ spied u" and + "Auth_PriK n \ B \ spied u \ B \ Auth_PriK n \ spied u" + by blast + hence "Auth_PriK n \ B \ parts (used u) \ B \ Auth_PriK n \ parts (used u)" + by blast + moreover have "B \ Auth_PriK n \ parts (used u)" + proof + assume "B \ Auth_PriK n \ parts (used u)" + hence "(\m. B = Auth_PriK m \ + (Asset m, \Num 2, PubKey (Auth_PriK n)\) \ u) \ + {PriKey B, PriKey (Auth_PriK n)} \ spied u" + by (rule parts_mult [OF C]) + then obtain m where "(Asset m, \Num 2, Auth_PubKey n\) \ u" + using E by auto + thus False + by (rule auth_pubkey_asset_ii [OF C]) + qed + ultimately have "Auth_PriK n \ B \ parts (used u)" by simp + hence "(\m. Auth_PriK n = Auth_PriK m \ + (Asset m, \Num 2, PubKey B\) \ u) \ + {PriKey (Auth_PriK n), PriKey B} \ spied u" + by (rule parts_mult [OF C]) + then obtain m where "Auth_PriK n = Auth_PriK m" and + "(Asset m, \Num 2, PubKey B\) \ u" + using E by auto + moreover from this have "Auth_PriKey m \ spied u \ + (\C SK. (Asset m, Token m (Auth_PriK m) B C SK) \ u)" + by (rule_tac asset_ii_spied [OF C G]) + ultimately show False + using E by simp +qed + +proposition asset_ii_secret: + "\s\<^sub>0 \ s; n \ bad_prikey; (Asset n, \Num 2, PubKey B\) \ s\ \ + PriKey B \ spied s" +by (rule notI, frule asset_ii_spied, assumption+, drule auth_prikey_secret, simp+) + + +proposition asset_i_secret [rule_format]: + assumes + A: "s\<^sub>0 \ s" and + B: "n \ bad_shakey" + shows "(Asset n, Crypt (Auth_ShaKey n) (PriKey S)) \ s \ + PriKey S \ spied s" +proof (rule rtrancl_induct [OF A], simp add: image_def, rule impI) + fix s s' + assume + C: "s\<^sub>0 \ s" and + D: "s \ s'" and + E: "(Asset n, Crypt (Auth_ShaKey n) (PriKey S)) \ s \ + PriKey S \ spied s" and + F: "(Asset n, Crypt (Auth_ShaKey n) (PriKey S)) \ s'" + show "PriKey S \ spied s'" + proof (insert D E F, auto simp add: rel_def) + assume "(Asset n, Crypt (ShaK (Auth_ShaK n)) (Key (PriK S))) \ s" + hence "(Asset n, Crypt (Auth_ShaKey n) (PriKey S)) \ s" by simp + hence "PriKey S \ used s" + by (rule asset_i_used [OF C, THEN mp]) + moreover assume "Key (PriK S) \ used s" + ultimately show False by simp + next + fix K + assume "(Spy, Crypt K (Key (PriK S))) \ s" + hence "Crypt K (PriKey S) \ parts (used s)" by auto + hence "(\m. K = Auth_ShaKey m \ + (Asset m, Crypt (Auth_ShaKey m) (PriKey S)) \ s) \ + {PriKey S, Key K} \ spied s" + (is "(\m. ?P m \ ?Q m) \ _") + by (rule parts_crypt_prikey [OF C]) + moreover assume "(Spy, Key (PriK S)) \ s" + ultimately obtain m where G: "?P m \ ?Q m" by auto + hence "?Q m" .. + moreover assume + "(Asset n, Crypt (ShaK (Auth_ShaK n)) (Key (PriK S))) \ s" + hence "(Asset n, Crypt (Auth_ShaKey n) (PriKey S)) \ s" by simp + ultimately have "m = n" + by (rule asset_i_unique [OF C]) + moreover assume "(Spy, Key (InvK K)) \ s" + ultimately have "Key (Auth_ShaKey n) \ spied s" + using G by simp + moreover have "Key (Auth_ShaKey n) \ spied s" + by (rule auth_shakey_secret [OF C B]) + ultimately show False by contradiction + next + fix B + assume "(Spy, S \ B) \ s" + hence "S \ B \ parts (used s)" by blast + hence "(\m. S = Auth_PriK m \ (Asset m, \Num 2, PubKey B\) \ s) \ + {PriKey S, PriKey B} \ spied s" + (is "(\m. ?P m \ _) \ _") + by (rule parts_mult [OF C]) + moreover assume "(Spy, Key (PriK S)) \ s" + ultimately obtain m where "?P m" by auto + moreover assume + "(Asset n, Crypt (ShaK (Auth_ShaK n)) (Key (PriK S))) \ s" + ultimately have "(Asset n, Crypt (Auth_ShaKey n) (Auth_PriKey m)) \ s" + by simp + thus False + by (rule auth_prikey_asset_i [OF C]) + next + fix A + assume "(Spy, A \ S) \ s" + hence "A \ S \ parts (used s)" by blast + hence "(\m. A = Auth_PriK m \ (Asset m, \Num 2, PubKey S\) \ s) \ + {PriKey A, PriKey S} \ spied s" + (is "(\m. _ \ ?P m) \ _") + by (rule parts_mult [OF C]) + moreover assume "(Spy, Key (PriK S)) \ s" + ultimately obtain m where "?P m" by auto + assume "(Asset n, Crypt (ShaK (Auth_ShaK n)) (Key (PriK S))) \ s" + hence "(Asset n, Crypt (Auth_ShaKey n) (PriKey S)) \ s" by simp + thus False + by (rule asset_i_asset_ii [OF C _ `?P m`]) + next + fix Y + assume "(Spy, \Key (PriK S), Y\) \ s" + hence "\PriKey S, Y\ \ parts (used s)" by auto + hence "{PriKey S, Y} \ spied s" + by (rule parts_mpair_key [OF C, where K = "PriK S"], simp) + moreover assume "(Spy, Key (PriK S)) \ s" + ultimately show False by simp + next + fix X + assume "(Spy, \X, Key (PriK S)\) \ s" + hence "\X, PriKey S\ \ parts (used s)" by auto + hence "{X, PriKey S} \ spied s" + by (rule parts_mpair_key [OF C, where K = "PriK S"], simp add: image_def) + moreover assume "(Spy, Key (PriK S)) \ s" + ultimately show False by simp + qed +qed + +proposition owner_ii_secret [rule_format]: + "s\<^sub>0 \ s \ + (Owner n, \Num 1, PubKey A\) \ s \ + PriKey A \ spied s" +proof (erule rtrancl_induct, simp add: image_def, rule impI) + fix s s' + assume + A: "s\<^sub>0 \ s" and + B: "s \ s'" and + C: "(Owner n, \Num 1, PubKey A\) \ s \ PriKey A \ spied s" and + D: "(Owner n, \Num 1, PubKey A\) \ s'" + show "PriKey A \ spied s'" + proof (insert B C D, auto simp add: rel_def) + assume "(Owner n, \Num (Suc 0), Key (PubK A)\) \ s" + hence "(Owner n, \Num 1, PubKey A\) \ s" by simp + hence "PriKey A \ used s" + by (rule owner_ii_used [OF A, THEN mp]) + moreover assume "Key (PriK A) \ used s" + ultimately show False by simp + next + fix K + assume "(Spy, Crypt K (Key (PriK A))) \ s" + hence "Crypt K (PriKey A) \ parts (used s)" by auto + hence "(\m. K = Auth_ShaKey m \ + (Asset m, Crypt (Auth_ShaKey m) (PriKey A)) \ s) \ + {PriKey A, Key K} \ spied s" + (is "(\m. _ \ ?P m) \ _") + by (rule parts_crypt_prikey [OF A]) + moreover assume "(Spy, Key (PriK A)) \ s" + ultimately obtain m where "?P m" by auto + moreover assume "(Owner n, \Num (Suc 0), Key (PubK A)\) \ s" + hence "(Owner n, \Num 1, PubKey A\) \ s" by simp + ultimately show False + by (rule asset_i_owner_ii [OF A]) + next + fix B + assume "(Spy, A \ B) \ s" + hence "A \ B \ parts (used s)" by blast + hence "(\m. A = Auth_PriK m \ (Asset m, \Num 2, PubKey B\) \ s) \ + {PriKey A, PriKey B} \ spied s" + (is "(\m. ?P m \ _) \ _") + by (rule parts_mult [OF A]) + moreover assume "(Spy, Key (PriK A)) \ s" + ultimately obtain m where "?P m" by auto + moreover assume "(Owner n, \Num (Suc 0), Key (PubK A)\) \ s" + ultimately have "(Owner n, \Num 1, Auth_PubKey m\) \ s" by simp + thus False + by (rule auth_pubkey_owner_ii [OF A]) + next + fix B + assume "(Spy, B \ A) \ s" + hence "B \ A \ parts (used s)" by blast + hence "(\m. B = Auth_PriK m \ (Asset m, \Num 2, PubKey A\) \ s) \ + {PriKey B, PriKey A} \ spied s" + (is "(\m. _ \ ?P m) \ _") + by (rule parts_mult [OF A]) + moreover assume "(Spy, Key (PriK A)) \ s" + ultimately obtain m where "?P m" by auto + moreover assume "(Owner n, \Num (Suc 0), Key (PubK A)\) \ s" + hence "(Owner n, \Num 1, PubKey A\) \ s" by simp + ultimately show False + by (rule asset_ii_owner_ii [OF A]) + next + fix Y + assume "(Spy, \Key (PriK A), Y\) \ s" + hence "\PriKey A, Y\ \ parts (used s)" by auto + hence "{PriKey A, Y} \ spied s" + by (rule parts_mpair_key [OF A, where K = "PriK A"], simp) + moreover assume "(Spy, Key (PriK A)) \ s" + ultimately show False by simp + next + fix X + assume "(Spy, \X, Key (PriK A)\) \ s" + hence "\X, PriKey A\ \ parts (used s)" by auto + hence "{X, PriKey A} \ spied s" + by (rule parts_mpair_key [OF A, where K = "PriK A"], simp add: image_def) + moreover assume "(Spy, Key (PriK A)) \ s" + ultimately show False by simp + qed +qed + +proposition seskey_spied [rule_format]: + "s\<^sub>0 \ s \ + SesKey SK \ spied s \ + (\S A C. fst SK = Some S \ A \ fst (snd SK) \ C \ snd (snd SK) \ + {PriKey S, PriKey A, PriKey C} \ spied s)" + (is "_ \ _ \ (\S A C. ?P S A C s)") +proof (erule rtrancl_induct, simp add: image_def, rule impI) + fix s s' + assume + A: "s\<^sub>0 \ s" and + B: "s \ s'" and + C: "SesKey SK \ spied s \ (\S A C. ?P S A C s)" and + D: "SesKey SK \ spied s'" + show "\S A C. ?P S A C s'" + proof (insert B C D, auto simp add: rel_def, blast, rule_tac [!] FalseE) + fix K + assume "(Spy, Crypt K (Key (SesK SK))) \ s" + hence "Crypt K (Key (SesK SK)) \ parts (used s)" by blast + hence "{Key (SesK SK), Key K} \ spied s" + by (rule parts_crypt_key [OF A], simp add: image_def) + moreover assume "(Spy, Key (SesK SK)) \ s" + ultimately show False by simp + next + fix Y + assume "(Spy, \Key (SesK SK), Y\) \ s" + hence "\SesKey SK, Y\ \ parts (used s)" by auto + hence "{SesKey SK, Y} \ spied s" + by (rule parts_mpair_key [OF A, where K = "SesK SK"], simp) + moreover assume "(Spy, Key (SesK SK)) \ s" + ultimately show False by simp + next + fix X + assume "(Spy, \X, Key (SesK SK)\) \ s" + hence "\X, SesKey SK\ \ parts (used s)" by auto + hence "{X, SesKey SK} \ spied s" + by (rule parts_mpair_key [OF A, where K = "SesK SK"], simp add: image_def) + moreover assume "(Spy, Key (SesK SK)) \ s" + ultimately show False by simp + qed +qed + +proposition owner_seskey_shakey: + assumes + A: "s\<^sub>0 \ s" and + B: "n \ bad_shakey" and + C: "(Owner n, SesKey SK) \ s" + shows "SesKey SK \ spied s" +proof + have "(\S. fst SK = Some S \ Crypt (Auth_ShaKey n) (PriKey S) \ used s) \ + fst SK = None" + (is "(\S. ?P S) \ _") + by (rule owner_seskey_nonce [OF A C]) + moreover assume "SesKey SK \ spied s" + hence D: "\S A C. fst SK = Some S \ A \ fst (snd SK) \ + C \ snd (snd SK) \ {PriKey S, PriKey A, PriKey C} \ spied s" + by (rule seskey_spied [OF A]) + ultimately obtain S where "?P S" by auto + hence "Crypt (Auth_ShaKey n) (PriKey S) \ parts (used s)" by blast + hence "(\m. Auth_ShaKey n = Auth_ShaKey m \ + (Asset m, Crypt (Auth_ShaKey m) (PriKey S)) \ s) \ + {PriKey S, Key (Auth_ShaKey n)} \ spied s" + (is "(\m. ?Q m \ ?R m) \ _") + by (rule parts_crypt_prikey [OF A]) + moreover have "Key (Auth_ShaKey n) \ spied s" + by (rule auth_shakey_secret [OF A B]) + ultimately obtain m where "?Q m" and "?R m" by blast + hence "m \ bad_shakey" + using B by simp + hence "PriKey S \ spied s" + by (rule asset_i_secret [OF A _ `?R m`]) + moreover have "PriKey S \ spied s" + using D and `?P S` by auto + ultimately show False by contradiction +qed + +proposition owner_seskey_prikey: + assumes + A: "s\<^sub>0 \ s" and + B: "n \ bad_prikey" and + C: "(Owner m, SesKey SK) \ s" and + D: "(Asset n, \Num 2, PubKey B\) \ s" and + E: "B \ fst (snd SK)" + shows "SesKey SK \ spied s" +proof + have "\A B C D. fst (snd SK) = {A, B} \ snd (snd SK) = {C, D} \ + (Owner m, \Num 1, PubKey A\) \ s \ + (Owner m, \Num 3, PubKey C\) \ s \ + (Owner m, Crypt (SesK SK) (PubKey D)) \ s" + (is "\A B C D. ?P A B \ _ \ ?Q A \ _") + by (rule owner_seskey_other [OF A C]) + then obtain A B' where "?P A B'" and "?Q A" by blast + assume "SesKey SK \ spied s" + hence "\S A' C. fst SK = Some S \ A' \ fst (snd SK) \ C \ snd (snd SK) \ + {PriKey S, PriKey A', PriKey C} \ spied s" + (is "\S A' C. _ \ ?R A' \ _") + by (rule seskey_spied [OF A]) + then obtain A' where "A' \ fst (snd SK)" and "PriKey A' \ spied s" (is "?R A'") + by blast + hence "{A', A, B} \ {A, B'}" + using E and `?P A B'` by simp + hence "card {A', A, B} \ card {A, B'}" + by (rule_tac card_mono, simp) + also have "\ \ Suc (Suc 0)" + by (rule card_insert_le_m1, simp_all) + finally have "card {A', A, B} \ Suc (Suc 0)" . + moreover have "card {A', A, B} = Suc (card {A, B})" + proof (rule card_insert_disjoint, simp_all, rule conjI, rule_tac [!] notI) + assume "A' = A" + hence "?R A" + using `?R A'` by simp + moreover have "\ ?R A" + by (rule owner_ii_secret [OF A `?Q A`]) + ultimately show False by contradiction + next + assume "A' = B" + hence "?R B" + using `?R A'` by simp + moreover have "\ ?R B" + by (rule asset_ii_secret [OF A B D]) + ultimately show False by contradiction + qed + moreover have "card {A, B} = Suc (card {B})" + proof (rule card_insert_disjoint, simp_all, rule notI) + assume "A = B" + hence "(Asset n, \Num 2, PubKey A\) \ s" + using D by simp + thus False + by (rule asset_ii_owner_ii [OF A _ `?Q A`]) + qed + ultimately show False by simp +qed + +proposition asset_seskey_shakey: + assumes + A: "s\<^sub>0 \ s" and + B: "n \ bad_shakey" and + C: "(Asset n, SesKey SK) \ s" + shows "SesKey SK \ spied s" +proof + have "\S. fst SK = Some S \ + (Asset n, Crypt (Auth_ShaKey n) (PriKey S)) \ s" + (is "\S. ?P S \ ?Q S") + by (rule asset_seskey_nonce [OF A C]) + then obtain S where "?P S" and "?Q S" by blast + have "PriKey S \ spied s" + by (rule asset_i_secret [OF A B `?Q S`]) + moreover assume "SesKey SK \ spied s" + hence "\S A C. fst SK = Some S \ A \ fst (snd SK) \ C \ snd (snd SK) \ + {PriKey S, PriKey A, PriKey C} \ spied s" + by (rule seskey_spied [OF A]) + hence "PriKey S \ spied s" + using `?P S` by auto + ultimately show False by contradiction +qed + + +theorem owner_seskey_unique: + assumes + A: "s\<^sub>0 \ s" and + B: "(Owner m, Crypt (SesK SK) (Pwd m)) \ s" and + C: "(Owner n, Crypt (SesK SK) (Pwd n)) \ s" + shows "m = n" +proof (rule ccontr) + have D: "(Owner m, SesKey SK) \ s \ + (\A B C. Token m A B C SK \ used s \ B \ fst (snd SK))" + (is "?P m \ (\A B C. ?Q m A B C)") + by (rule owner_v_state [OF A B]) + hence "?P m" by blast + hence "\A B C D. fst (snd SK) = {A, B} \ snd (snd SK) = {C, D} \ + (Owner m, \Num 1, PubKey A\) \ s \ + (Owner m, \Num 3, PubKey C\) \ s \ + (Owner m, Crypt (SesK SK) (PubKey D)) \ s" + (is "\A B C D. ?R A B \ ?S C D \ ?T m A \ ?U m C D") + by (rule owner_seskey_other [OF A]) + then obtain A B where "?R A B" and "?T m A" by blast + have "?P n \ (\A B C. ?Q n A B C)" + by (rule owner_v_state [OF A C]) + hence "?P n" by blast + hence "\A B C D. ?R A B \ ?S C D \ ?T n A \ ?U n C D" + by (rule owner_seskey_other [OF A]) + then obtain A' B' where "?R A' B'" and "?T n A'" by blast + from D obtain A'' B'' C where "?Q m A'' B'' C" by blast + hence "Token m A'' B'' C SK \ parts (used s)" by blast + hence "Crypt (SesK SK) (A'' \ B'') \ parts (used s)" by blast + hence "B'' \ fst (snd SK) \ + (\i C'. (Asset i, Token i (Auth_PriK i) B'' C' SK) \ s) \ + {A'' \ B'', SesKey SK} \ spied s" + (is "?V B'' \ (\i C'. ?W i B'' C') \ _") + by (rule parts_crypt_mult [OF A]) + hence "\D. ?V D \ D \ {A, A'}" + proof (rule disjE, (erule_tac conjE, ((erule_tac exE)+)?)+) + fix i C' + assume "?V B''" and "?W i B'' C'" + have "\A D. ?R A B'' \ ?S C' D \ + (Asset i, \Num 2, PubKey B''\) \ s \ (Asset i, \Num 4, PubKey D\) \ s \ + Crypt (SesK SK) (PubKey D) \ used s \ (Asset i, PubKey B'') \ s" + (is "\A D. _ \ _ \ ?X i B'' \ _") + by (rule asset_iv_state [OF A `?W i B'' C'`]) + hence "?X i B''" by blast + have "B'' \ A" + proof + assume "B'' = A" + hence "?X i A" + using `?X i B''` by simp + thus False + by (rule asset_ii_owner_ii [OF A _ `?T m A`]) + qed + moreover have "B'' \ A'" + proof + assume "B'' = A'" + hence "?X i A'" + using `?X i B''` by simp + thus False + by (rule asset_ii_owner_ii [OF A _ `?T n A'`]) + qed + ultimately show ?thesis + using `?V B''` by blast + next + assume "{A'' \ B'', SesKey SK} \ spied s" + hence "SesKey SK \ spied s" by simp + hence "\S D E. fst SK = Some S \ ?V D \ E \ snd (snd SK) \ + {PriKey S, PriKey D, PriKey E} \ spied s" + by (rule seskey_spied [OF A]) + then obtain D where "?V D" and "PriKey D \ spied s" (is "?X D") + by blast + moreover have "D \ A" + proof + assume "D = A" + hence "?X A" + using `?X D` by simp + moreover have "\ ?X A" + by (rule owner_ii_secret [OF A `?T m A`]) + ultimately show False by contradiction + qed + moreover have "D \ A'" + proof + assume "D = A'" + hence "?X A'" + using `?X D` by simp + moreover have "\ ?X A'" + by (rule owner_ii_secret [OF A `?T n A'`]) + ultimately show False by contradiction + qed + ultimately show ?thesis by blast + qed + then obtain D where "?V D" and E: "D \ {A, A'}" by blast + hence "{D, A, A'} \ {A, B}" + using `?R A B` and `?R A' B'` by blast + hence "card {D, A, A'} \ card {A, B}" + by (rule_tac card_mono, simp) + also have "\ \ Suc (Suc 0)" + by (rule card_insert_le_m1, simp_all) + finally have "card {D, A, A'} \ Suc (Suc 0)" . + moreover have "card {D, A, A'} = Suc (card {A, A'})" + by (rule card_insert_disjoint [OF _ E], simp) + moreover assume "m \ n" + hence "card {A, A'} = Suc (card {A'})" + proof (rule_tac card_insert_disjoint, simp_all, erule_tac contrapos_nn) + assume "A = A'" + hence "?T n A" + using `?T n A'` by simp + thus "m = n" + by (rule owner_ii_unique [OF A `?T m A`]) + qed + ultimately show False by simp +qed + + +theorem owner_seskey_secret: + assumes + A: "s\<^sub>0 \ s" and + B: "n \ bad_shakey \ bad_prikey" and + C: "(Owner n, Crypt (SesK SK) (Pwd n)) \ s" + shows "SesKey SK \ spied s" +proof - + have "(Owner n, SesKey SK) \ s \ + (\A B C. Token n A B C SK \ used s \ B \ fst (snd SK))" + (is "?P \ (\A B C. ?Q A B C \ ?R B)") + by (rule owner_v_state [OF A C]) + then obtain A B C where "?P" and "?Q A B C" and "?R B" by blast + have "n \ bad_shakey \ n \ bad_shakey" by simp + moreover { + assume "n \ bad_shakey" + hence D: "n \ bad_prikey" + using B by simp + hence "Auth_PriKey n \ spied s" + by (rule auth_prikey_secret [OF A]) + moreover have "Sign n A \ parts (used s)" + using `?Q A B C` by blast + hence "A = Auth_PriK n" + by (rule parts_sign [OF A]) + hence "?Q (Auth_PriK n) B C" + using `?Q A B C` by simp + hence "Auth_PriK n \ B \ parts (used s)" by blast + hence "(\m. Auth_PriK n = Auth_PriK m \ + (Asset m, \Num 2, PubKey B\) \ s) \ + {PriKey (Auth_PriK n), PriKey B} \ spied s" + (is "(\m. ?S m \ ?T m) \ _") + by (rule parts_mult [OF A]) + ultimately obtain m where "?S m" and "?T m" by auto + hence "m \ bad_prikey" + using D by simp + hence ?thesis + by (rule owner_seskey_prikey [OF A _ `?P` `?T m` `?R B`]) + } + moreover { + assume "n \ bad_shakey" + hence ?thesis + by (rule owner_seskey_shakey [OF A _ `?P`]) + } + ultimately show ?thesis .. +qed + + +theorem owner_num_genuine: + assumes + A: "s\<^sub>0 \ s" and + B: "n \ bad_shakey \ bad_prikey" and + C: "(Owner n, Crypt (SesK SK) (Pwd n)) \ s" and + D: "Crypt (SesK SK) (Num 0) \ used s" + shows "(Asset n, Crypt (SesK SK) (Num 0)) \ s" +proof - + have "Crypt (SesK SK) (Num 0) \ parts (used s)" + using D .. + hence "(\m. (Asset m, Crypt (SesK SK) (Num 0)) \ s) \ + SesKey SK \ spied s" + by (rule parts_crypt_num [OF A]) + moreover have E: "SesKey SK \ spied s" + by (rule owner_seskey_secret [OF A B C]) + ultimately obtain m where "(Asset m, Crypt (SesK SK) (Num 0)) \ s" + by blast + moreover from this have "(Asset m, SesKey SK) \ s \ + Crypt (SesK SK) (Pwd m) \ used s" + by (rule asset_v_state [OF A]) + hence "Crypt (SesK SK) (Pwd m) \ parts (used s)" by blast + hence "(\SK'. SesK SK = SesK SK' \ + (Owner m, Crypt (SesK SK') (Pwd m)) \ s) \ + {Pwd m, Key (SesK SK)} \ spied s" + by (rule parts_crypt_pwd [OF A]) + hence "(Owner m, Crypt (SesK SK) (Pwd m)) \ s" + using E by simp + hence "m = n" + by (rule owner_seskey_unique [OF A _ C]) + ultimately show ?thesis by simp +qed + + +theorem owner_token_genuine: + assumes + A: "s\<^sub>0 \ s" and + B: "n \ bad_shakey \ bad_prikey" and + C: "(Owner n, \Num 3, PubKey C\) \ s" and + D: "(Owner n, Crypt (SesK SK) (Pwd n)) \ s" and + E: "Token n A B C SK \ used s" + shows "A = Auth_PriK n \ B \ fst (snd SK) \ C \ snd (snd SK) \ + (Asset n, \Num 2, PubKey B\) \ s \ (Asset n, Token n A B C SK) \ s" + (is "?P n A \ ?Q B \ ?R C \ ?S n B \ _") +proof - + have "Crypt (SesK SK) (Sign n A) \ parts (used s)" + using E by blast + hence "(Asset n, SesKey SK) \ s \ SesKey SK \ spied s" + by (rule parts_crypt_sign [OF A]) + moreover have "SesKey SK \ spied s" + by (rule owner_seskey_secret [OF A B D]) + ultimately have "(Asset n, SesKey SK) \ s" by simp + hence "\A B C D. fst (snd SK) = {A, B} \ snd (snd SK) = {C, D} \ + ?S n B \ (Asset n, \Num 4, PubKey D\) \ s \ + (Asset n, Token n (Auth_PriK n) B C SK) \ s" + (is "\A B C D. ?T A B \ ?U C D \ _ \ ?V n D \ ?W n B C") + by (rule asset_seskey_other [OF A]) + then obtain A' B' C' D where + "?T A' B'" and "?U C' D" and "?S n B'" and "?V n D" and "?W n B' C'" + by blast + have "Sign n A \ parts (used s)" + using E by blast + hence "?P n A" + by (rule parts_sign [OF A]) + have "Crypt (SesK SK) (A \ B) \ parts (used s)" + using E by blast + hence "?Q B \ (\m C''. ?W m B C'') \ {A \ B, SesKey SK} \ spied s" + by (rule parts_crypt_mult [OF A]) + moreover have F: "SesKey SK \ spied s" + by (rule owner_seskey_secret [OF A B D]) + ultimately obtain m C'' where "?Q B" and "?W m B C''" by blast + have "\A D. ?T A B \ ?U C'' D \ ?S m B \ ?V m D \ + Crypt (SesK SK) (PubKey D) \ used s \ (Asset m, PubKey B) \ s" + by (rule asset_iv_state [OF A `?W m B C''`]) + hence "?S m B" by blast + have "(Owner n, SesKey SK) \ s \ + (\A B C. Token n A B C SK \ used s \ B \ fst (snd SK))" + by (rule owner_v_state [OF A D]) + hence "(Owner n, SesKey SK) \ s" by blast + hence "\A B C D. ?T A B \ ?U C D \ + (Owner n, \Num 1, PubKey A\) \ s \ + (Owner n, \Num 3, PubKey C\) \ s \ + (Owner n, Crypt (SesK SK) (PubKey D)) \ s" + (is "\A B C D. _ \ _ \ ?X A \ _") + by (rule owner_seskey_other [OF A]) + then obtain A'' where "?Q A''" and "?X A''" by blast + have G: "B' = B" + proof (rule ccontr) + have "{A'', B', B} \ {A', B'}" + using `?T A' B'` and `?Q B` and `?Q A''` by simp + hence "card {A'', B', B} \ card {A', B'}" + by (rule_tac card_mono, simp) + also have "\ \ Suc (Suc 0)" + by (rule card_insert_le_m1, simp_all) + finally have "card {A'', B', B} \ Suc (Suc 0)" . + moreover have "A'' \ {B', B}" + proof (simp, rule conjI, rule_tac [!] notI) + assume "A'' = B'" + hence "?S n A''" + using `?S n B'` by simp + thus False + by (rule asset_ii_owner_ii [OF A _ `?X A''`]) + next + assume "A'' = B" + hence "?S m A''" + using `?S m B` by simp + thus False + by (rule asset_ii_owner_ii [OF A _ `?X A''`]) + qed + hence "card {A'', B', B} = Suc (card {B', B})" + by (rule_tac card_insert_disjoint, simp) + moreover assume "B' \ B" + hence "card {B', B} = Suc (card {B})" + by (rule_tac card_insert_disjoint, simp_all) + ultimately show False by simp + qed + hence "?S n B" + using `?S n B'` by simp + have "Crypt (SesK SK) (PubKey C) \ parts (used s)" + using E by blast + hence "?R C \ ((\n. (Owner n, SesKey SK) \ s) \ (\n B. ?W n B C)) \ + SesKey SK \ spied s" + by (rule parts_crypt_pubkey [OF A]) + hence "?R C" + using F by simp + hence "C \ {C', D}" + using `?U C' D` by simp + moreover have "C \ D" + proof + assume "C = D" + hence "?V n C" + using `?V n D` by simp + thus False + by (rule asset_iii_owner_iii [OF A _ C]) + qed + ultimately have "C = C'" by simp + hence "(Asset n, Token n A B C SK) \ s" + using G and `?P n A` and `?W n B' C'` by simp + thus ?thesis + using `?P n A` and `?Q B` and `?R C` and `?S n B` by simp +qed + + +theorem pwd_secret: + assumes + A: "s\<^sub>0 \ s" and + B: "n \ bad_pwd \ bad_shakey \ bad_prikey" + shows "Pwd n \ spied s" +proof (rule rtrancl_induct [OF A], insert B, simp add: image_def) + fix s s' + assume + C: "s\<^sub>0 \ s" and + D: "s \ s'" and + E: "Pwd n \ spied s" + show "Pwd n \ spied s'" + proof (insert D E, auto simp add: rel_def) + fix K + assume "(Spy, Crypt K (Pwd n)) \ s" + hence "Crypt K (Pwd n) \ parts (used s)" by blast + hence "(\SK. K = SesK SK \ (Owner n, Crypt (SesK SK) (Pwd n)) \ s) \ + {Pwd n, Key K} \ spied s" + (is "(\SK. ?P SK \ ?Q SK) \ _") + by (rule parts_crypt_pwd [OF C]) + then obtain SK where "?P SK" and "?Q SK" + using E by blast + have "n \ bad_shakey \ bad_prikey" + using B by simp + hence "SesKey SK \ spied s" + by (rule owner_seskey_secret [OF C _ `?Q SK`]) + moreover assume "(Spy, Key (InvK K)) \ s" + ultimately show False + using `?P SK` by simp + next + fix Y + assume "(Spy, \Pwd n, Y\) \ s" + hence "\Pwd n, Y\ \ parts (used s)" by blast + hence "{Pwd n, Y} \ spied s" + by (rule parts_mpair_pwd [OF C, where n = n], simp) + with E show False by simp + next + fix X + assume "(Spy, \X, Pwd n\) \ s" + hence "\X, Pwd n\ \ parts (used s)" by blast + hence "{X, Pwd n} \ spied s" + by (rule parts_mpair_pwd [OF C, where n = n], simp) + with E show False by simp + qed +qed + + +theorem asset_seskey_unique: + assumes + A: "s\<^sub>0 \ s" and + B: "(Asset m, Token m (Auth_PriK m) B' C' SK) \ s" and + C: "(Asset n, Token n (Auth_PriK n) B C SK) \ s" + (is "?P n B C SK s") + shows "m = n \ B' = B \ C' = C" +proof (subst (2) cases_simp [of "B' = B", symmetric], simp, rule conjI, rule impI, + insert B C, simp only:, drule asset_iv_unique [OF A], simp, simp, rule ccontr) + assume "B' \ B" + moreover have "\A D. fst (snd SK) = {A, B'} \ snd (snd SK) = {C', D} \ + (Asset m, \Num 2, PubKey B'\) \ s \ (Asset m, \Num 4, PubKey D\) \ s \ + Crypt (SesK SK) (PubKey D) \ used s \ (Asset m, PubKey B') \ s" + (is "?Q m B' C'") + by (rule asset_iv_state [OF A B]) + then obtain A where "fst (snd SK) = {A, B'}" and + "(Asset m, \Num 2, PubKey B'\) \ s" + by blast + moreover have "?Q n B C" + by (rule asset_iv_state [OF A C]) + hence "B \ fst (snd SK)" and "(Asset n, \Num 2, PubKey B\) \ s" + by auto + ultimately have D: "\A \ fst (snd SK). + \i C. (Asset i, \Num 2, PubKey A\) \ s \ ?P i A C SK s" + using B and C by auto + have "Crypt (SesK SK) (PubKey C) \ parts (used s)" + using C by blast + thus False + proof (rule parts_pubkey_false [OF A], rule_tac allI, rule_tac [!] notI) + fix i + assume "(Owner i, SesKey SK) \ s" + hence "\A B C D. fst (snd SK) = {A, B} \ snd (snd SK) = {C, D} \ + (Owner i, \Num 1, PubKey A\) \ s \ + (Owner i, \Num 3, PubKey C\) \ s \ + (Owner i, Crypt (SesK SK) (PubKey D)) \ s" + by (rule owner_seskey_other [OF A]) + then obtain A where "A \ fst (snd SK)" and + E: "(Owner i, \Num 1, PubKey A\) \ s" + by blast + then obtain j where "(Asset j, \Num 2, PubKey A\) \ s" + using D by blast + thus False + by (rule asset_ii_owner_ii [OF A _ E]) + next + assume "SesKey SK \ spied s" + hence "\S A C. fst SK = Some S \ A \ fst (snd SK) \ C \ snd (snd SK) \ + {PriKey S, PriKey A, PriKey C} \ spied s" + (is "?R s") + by (rule seskey_spied [OF A]) + moreover have "\ (\A \ fst (snd SK). PriKey A \ spied s)" + (is "\ ?S s") + proof + assume "?S s" + moreover have "\ ?S s\<^sub>0" + by (subst bex_simps, rule ballI, drule bspec [OF D], (erule exE)+, + erule conjE, rule asset_ii_init [OF A]) + ultimately have "\u v. s\<^sub>0 \ u \ u \ v \ v \ s \ \ ?S u \ ?S v" + by (rule rtrancl_start [OF A]) + then obtain u v A where E: "s\<^sub>0 \ u" and F: "u \ v" and G: "v \ s" and + H: "\ ?S u" and I: "A \ fst (snd SK)" and J: "PriKey A \ spied u" and + K: "PriKey A \ spied v" + by blast + then obtain i where "(Asset i, \Num 2, PubKey A\) \ s" + using D by blast + hence "(Asset i, \Num 2, PubKey A\) \ v" + proof (rule_tac ccontr, drule_tac rtrancl_start [OF G], simp, + (erule_tac exE)+, (erule_tac conjE)+) + fix w x + assume "w \ x" and "(Asset i, \Num 2, PubKey A\) \ w" and + "(Asset i, \Num 2, PubKey A\) \ x" + hence "PriKey A \ spied w" + by (auto simp add: rel_def) + moreover assume "v \ w" + hence "PriKey A \ spied w" + by (rule_tac rev_subsetD [OF K], rule spied_subset) + ultimately show False by contradiction + qed + hence "(Asset i, \Num 2, PubKey A\) \ u" + using F and K by (auto simp add: rel_def) + hence "Auth_PriKey i \ spied u \ (\C SK. ?P i A C SK u)" + by (rule asset_ii_spied_start [OF E F K J]) + then obtain C' SK' where L: "?P i A C' SK' u" by blast + moreover have M: "u \ s" + using F and G by simp + ultimately have "?P i A C' SK' s" + by (erule_tac rev_subsetD, rule_tac state_subset) + moreover obtain j C where "?P j A C SK s" + using D and I by blast + ultimately have "i = j \ C' = C \ SK' = SK" + by (rule asset_iv_unique [OF A]) + hence "Crypt (SesK SK) (PubKey C) \ parts (used u)" + using L by blast + thus False + proof (rule parts_pubkey_false [OF E], rule_tac allI, rule_tac [!] notI) + fix i + assume "(Owner i, SesKey SK) \ u" + hence "\A B C D. fst (snd SK) = {A, B} \ snd (snd SK) = {C, D} \ + (Owner i, \Num 1, PubKey A\) \ u \ + (Owner i, \Num 3, PubKey C\) \ u \ + (Owner i, Crypt (SesK SK) (PubKey D)) \ u" + by (rule owner_seskey_other [OF E]) + then obtain A where "A \ fst (snd SK)" and + N: "(Owner i, \Num 1, PubKey A\) \ u" + by blast + then obtain j where "(Asset j, \Num 2, PubKey A\) \ s" + using D by blast + moreover have "(Owner i, \Num 1, PubKey A\) \ s" + by (rule rev_subsetD [OF N], rule state_subset [OF M]) + ultimately show False + by (rule asset_ii_owner_ii [OF A]) + next + assume "SesKey SK \ spied u" + hence "?R u" + by (rule seskey_spied [OF E]) + thus False + using H by blast + qed + qed + ultimately show False by blast + qed +qed + + +theorem asset_seskey_secret: + assumes + A: "s\<^sub>0 \ s" and + B: "n \ bad_shakey \ (bad_pwd \ bad_prikey)" and + C: "(Asset n, Crypt (SesK SK) (Num 0)) \ s" + shows "SesKey SK \ spied s" +proof - + have D: "(Asset n, SesKey SK) \ s \ Crypt (SesK SK) (Pwd n) \ used s" + by (rule asset_v_state [OF A C]) + have "n \ bad_shakey \ n \ bad_shakey" by simp + moreover { + assume "n \ bad_shakey" + hence "Pwd n \ spied s" + using B by (rule_tac pwd_secret [OF A], simp) + moreover have "Crypt (SesK SK) (Pwd n) \ parts (used s)" + using D by blast + hence "(\SK'. SesK SK = SesK SK' \ + (Owner n, Crypt (SesK SK') (Pwd n)) \ s) \ + {Pwd n, Key (SesK SK)} \ spied s" + by (rule parts_crypt_pwd [OF A]) + ultimately have "(Owner n, Crypt (SesK SK) (Pwd n)) \ s" by simp + hence ?thesis + using B by (rule_tac owner_seskey_secret [OF A], simp_all) + } + moreover { + assume "n \ bad_shakey" + hence ?thesis + using D by (rule_tac asset_seskey_shakey [OF A], simp_all) + } + ultimately show ?thesis .. +qed + + +theorem asset_pwd_genuine: + assumes + A: "s\<^sub>0 \ s" and + B: "n \ bad_shakey \ (bad_pwd \ bad_prikey)" and + C: "(Asset n, Crypt (SesK SK) (Num 0)) \ s" + shows "(Owner n, Crypt (SesK SK) (Pwd n)) \ s" +proof - + have "(Asset n, SesKey SK) \ s \ Crypt (SesK SK) (Pwd n) \ used s" + by (rule asset_v_state [OF A C]) + hence "Crypt (SesK SK) (Pwd n) \ parts (used s)" by blast + hence "(\SK'. SesK SK = SesK SK' \ + (Owner n, Crypt (SesK SK') (Pwd n)) \ s) \ + {Pwd n, Key (SesK SK)} \ spied s" + by (rule parts_crypt_pwd [OF A]) + moreover have "SesKey SK \ spied s" + by (rule asset_seskey_secret [OF A B C]) + ultimately show ?thesis by simp +qed + + +theorem asset_token_genuine: + assumes + A: "s\<^sub>0 \ s" and + B: "n \ bad_shakey \ (bad_pwd \ bad_prikey)" and + C: "(Asset n, \Num 4, PubKey D\) \ s" and + D: "(Asset n, Crypt (SesK SK) (Num 0)) \ s" and + E: "D \ snd (snd SK)" + shows "(Owner n, Crypt (SesK SK) (PubKey D)) \ s" +proof - + have "(Owner n, Crypt (SesK SK) (Pwd n)) \ s" + by (rule asset_pwd_genuine [OF A B D]) + hence "(Owner n, SesKey SK) \ s \ + (\A B C. Token n A B C SK \ used s \ B \ fst (snd SK))" + by (rule owner_v_state [OF A]) + hence "(Owner n, SesKey SK) \ s" .. + hence "\A B C D. fst (snd SK) = {A, B} \ snd (snd SK) = {C, D} \ + (Owner n, \Num 1, PubKey A\) \ s \ + (Owner n, \Num 3, PubKey C\) \ s \ + (Owner n, Crypt (SesK SK) (PubKey D)) \ s" + (is "\A B C D. _ \ ?P C D \ _ \ ?Q C \ ?R D") + by (rule owner_seskey_other [OF A]) + then obtain C D' where "?P C D'" and "?Q C" and "?R D'" by blast + have "D \ C" + proof + assume "D = C" + hence "?Q D" + using `?Q C` by simp + thus False + by (rule asset_iii_owner_iii [OF A C]) + qed + hence "D = D'" + using E and `?P C D'` by simp + thus ?thesis + using `?R D'` by simp +qed + + +end diff --git a/thys/Relational_Method/Definitions.thy b/thys/Relational_Method/Definitions.thy new file mode 100644 --- /dev/null +++ b/thys/Relational_Method/Definitions.thy @@ -0,0 +1,852 @@ +(* Title: The Relational Method with Message Anonymity for the Verification of Cryptographic Protocols + Author: Pasquale Noce + Software Engineer at HID Global, Italy + pasquale dot noce dot lavoro at gmail dot com + pasquale dot noce at hidglobal dot com +*) + +section "The relational method and message anonymity" + +theory Definitions + imports Main +begin + +text \ +\null + +\emph{This paper is dedicated to my mother, my favourite chess opponent -- in addition to being many +other wonderful things!} +\ + + +subsection "Introduction" + +text \ +As Bertrand Russell says in the last pages of \emph{A History of Western Philosophy}, a distinctive +feature of science is that "we can make successive approximations to the truth, in which each new +stage results from an improvement, not a rejection, of what has gone before". When dealing with a +formal verification method for information processing systems, such as Paulson's inductive method +for the verification of cryptographic protocols (cf. @{cite "Paulson98"}, @{cite "Paulson20"}), a +more modest goal for this iterative improvement process, yet of significant practical importance, is +to streamline the definitions and proofs needed to model such a system and verify its properties. + +With this aim, specially when it comes to verifying protocols using public key cryptography, this +paper proposes an enhancement of the inductive method, named \emph{relational method} for reasons +clarified in what follows, and puts it into practice by verifying a sample protocol. This new method +is the result of some changes to the way how events, states, spy's capabilities, and the protocol +itself are formalized in the inductive method. Here below is a description of these changes, along +with a rationale for them. + + \<^descr>[Events.] In the inductive method, the fundamental building blocks of cryptographic protocols are +events of the form @{text "Says A B X"}, where @{text X} is a message being exchanged, @{text A} is +the agent that sends it, and @{text B} is the agent to which it is addressed. +\\However, any exchanged message can be intercepted by the spy and forwarded to any other agent, so +its intended recipient is not relevant for the protocol \emph{security} correctness -- though of +course being relevant for the protocol \emph{functional} correctness. Moreover, a legitimate agent +may also generate messages, e.g. ephemeral private keys, that she will never exchange with any other +agent. To model such an event, a datatype constructor other than @{text Says} should be used. How to +make things simpler? +\\The solution adopted in the relational method is to model events just as ordered pairs of the form +@{text "(A, X)"}, where @{text A} is an agent and @{text X} is a message. If event @{text "(A, X)"} +stands for @{text A}'s sending of @{text X} to another agent, where @{text A} is a legitimate agent, +then this event will be accompanied by event @{text "(Spy, X)"}, representing the spy's interception +of @{text X}. If event @{text "(A, X)"} rather stands for @{text A}'s generation of private message +@{text X}, e.g. an ephemeral private key, for her own exclusive use -- and if the spy has not hacked +@{text A} so as to steal her private messages as well --, then no companion event @{text "(Spy, X)"} +will occur instead. + + \<^descr>[States.] In the inductive method, the possible states of a cryptographic protocol are modeled as +event \emph{traces}, i.e. lists, and the protocol itself is formalized as a set of such traces. +Consequently, the protocol rules and security properties are expressed as formulae satisfied by any +event trace @{text evs} belonging to this set. +\\However, these formulae are such that their truth values depend only on the events contained in +@{text evs}, rather than on the actual order in which they occur -- in fact, robust protocol rules +and security properties cannot depend on the exact sequence of message exchanges in a scenario where +the spy can freely intercept and forward messages, or even generate and send her own ones. Thus, one +library function, @{const set}, and two custom recursive functions, @{text used} and @{text knows}, +are needed to convert event traces into event sets and message sets, respectively. +\\In the relational method, protocol states are simply modeled as event sets, so that the occurrence +of event @{text "(A, X)"} in state @{text s} can be expressed as the transition to the augmented +state @{term "insert (A, X) s"}. Hence, states consist of relations between agents and messages. As +a result, function @{const set} need not be used any longer, whereas functions @{text used} and +@{text spied} -- the latter one being a replacement for @{text "knows Spy"} --, which take a state +@{text s} as input, are mere abbreviations for @{term "Range s"} and @{term "s `` {Spy}"}. + + \<^descr>[Spy's capabilities.] In the inductive method, the spy's attack capabilities are formalized via +two inductively defined functions, @{text analz} and @{text synth}, used to construct the sets of +all the messages that the spy can learn -- @{text "analz (knows Spy evs)"} -- and send to legitimate +agents -- @{text "synth (analz (knows Spy evs))"} -- downstream of event trace @{text evs}. +\\Indeed, the introduction of these functions goes in the direction of decoupling the formalization +of the spy's capabilities from that of the protocol itself, consistently with the fact that what the +spy can do is independent of how the protocol works -- which only matters when it comes to verifying +protocol security. +\\In principle, this promises to provide a relevant benefit: these functions need to be defined, and +their properties to be proven, just once, whereupon such definitions and properties can be reused in +the formalization and verification of whatever protocol. +\\In practice, since both functions are of type @{text "msg set \ msg set"}, where @{text msg} is +the datatype defining all possible message formats, this benefit only applies as long as message +formats remain unchanged. However, when it comes to verifying a protocol making use of public key +cryptography, some new message format, and consequently some new related spy's capability as well, +are likely to be required. An example of this will be provided right away by the protocol considered +in this paper. +\\In the relational method, the representation of events as agent-message pairs offers a simpler way +to model the spy's capabilities, namely as supplementary protocol rules, analogous to the inductive +method's @{text Fake} rule, augmenting a state by one or more events of the form @{text "(Spy, X)"}. +In addition to eliminating the need for functions @{text analz} and @{text synth} -- which, in light +of the above considerations, does not significantly harm reusability --, this choice also abolishes +any distinction between what the spy can learn and what she can send. In fact, a state containing +event @{text "(Spy, X)"} is interpreted as one where the spy both knows message @{text X} and may +have sent it to whatever legitimate agent. Actually, this formalizes the facts that a real-world +attacker is free to send any message she has learned to any other party, and conversely to use any +message she has generated to further augment her knowledge. +\\In the inductive method, the former fact is modeled by property @{term "H \ synth H"} of function +@{text synth}, but the latter one has no formal counterpart, as in general @{term "H \ synth H"}. +This limitation on the spy's capabilities is not significant as long as the protocol makes use of +static keys only, but it is if session keys or ephemeral key pairs are generated -- as happens in +key establishment protocols, even in those using symmetric cryptography alone. In any such case, a +realistic spy must also be able to learn from anything she herself has generated, such as a nonce or +an ephemeral private key -- a result achieved without effort in the relational method. +\\An additional, nontrivial problem for the inductive method is that many protocols, including key +establishment ones, require the spy to be able to generate \emph{fresh} ephemeral messages only, as +otherwise the spy could succeed in breaking the protocol by just guessing the ephemeral messages +already generated at random by some legitimate agent -- a quite unrealistic attack pattern, provided +that such messages vary in a sufficiently wide range. At first glance, this need could be addressed +by extending the inductive definition of function @{text synth} with introduction rules of the form +@{term "Nonce n \ H \ Nonce n \ synth H"} or @{term "PriKey A \ H \ PriKey A \ synth H"}. +However, private ephemeral messages are not in general included in @{text "analz (knows Spy evs)"}, +since nonces may be encrypted with uncompromised keys when exchanged and private keys are usually +not exchanged at all, so this approach would not work. The only satisfactory alternative would be to +change the signature of function @{text synth}, e.g. by adding a second input message set @{text H'} +standing for @{text "used evs"}, or else by replacing @{text H} with event trace @{text evs} itself, +but this would render the function definition much more convoluted -- a problem easily bypassed in +the relational method. + + \<^descr>[Protocol.] In the inductive method, a cryptographic protocol consists of an inductively defined +set of event traces. This enables to prove the protocol security properties by induction using the +induction rule automatically generated as a result of such an inductive definition, i.e. by means of +\emph{rule induction}. Actually, this feature is exactly what gives the method its very name. Hence, +a consistent way to name a protocol verification method using some other form of induction would be +to replace adjective "inductive" with another one referring to that form of induction. +\\The relational method owes its name to this consideration. In this method, the introduction rules +defining \emph{protocol rules}, i.e. the possible transitions between protocol states, are replaced +with \emph{relations} between states, henceforth named \emph{protocol relations}. That is, for any +two states @{text s} and @{text s'}, there exists a transition leading from @{text s} to @{text s'} +just in case the ordered pair @{term "(s, s')"} is contained in at least one protocol relation -- +a state of affairs denoted using infix notation @{text "s \ s'"}. Then, the inductively defined set +itself is replaced with the \emph{reflexive transitive closure} of the union of protocol relations. +Namely, any state @{text s} may be reached from \emph{initial state} @{text s\<^sub>0}, viz. is a possible +protocol state, just in case pair @{term "(s\<^sub>0, s)"} lies within this reflexive transitive closure -- +a state of affairs denoted using infix notation @{text "s\<^sub>0 \ s"}. As a result, rule induction is +replaced with induction over reflexive transitive closures via rule @{thm [source] rtrancl_induct}, +which is the circumstance that originates the method name. +\\These changes provide the following important benefits. + + \<^item> Inserting and modifying the formal definition of a protocol is much more comfortable. In fact, +any change even to a single introduction rule within a monolithic inductive set definition entails a +re-evaluation of the whole definition, whereas each protocol relation will have its own stand-alone +definition, which also makes it easier to find errors. This advantage may go almost unnoticed for a +very simple protocol providing for just a few protocol rules, but gets evident in case of a complex +protocol. An example of this will be provided by the protocol considered in this paper: when looking +at the self-contained abbreviations used to define protocol relations, the reader will easily grasp +how much more convoluted an equivalent inductive set definition would have been. + + \<^item> In addition to induction via rule @{thm [source] rtrancl_induct}, a further powerful reasoning +pattern turns out to be available. It is based on the following general rule applying to reflexive +transitive closures (indeed, a rule so general and useful that it could rightfully become part of +the standard library), later on proven and assigned the name @{text rtrancl_start}: +@{prop [display] "\(x, y) \ r\<^sup>*; P y; \ P x\ \ +\u v. (x, u) \ r\<^sup>* \ (u, v) \ r \ (v, y) \ r\<^sup>* \ \ P u \ P v"} +In natural language, this rule states that for any chain of elements linked by a relation, if some +predicate is false for the first element of the chain and true for the last one, there must exist a +link in the chain where the predicate becomes true. +\\This rule can be used to prove propositions of the form @{text "\s \ s'; P s'[; Q]\ \ R s'"} for +any state @{text s} and predicate @{text P} such that @{term "\ P s"}, with an optional additional +assumption @{text Q}, without resorting to induction. Notably, \emph{regularity lemmas} have exactly +this form, where @{term "s = s\<^sub>0"}, @{term "P = (\s. X \ parts (used s))"} for some term @{text X} of +type @{text msg}, and @{text Q}, if present, puts some constraint on @{text X} or its components. +\\Such a proof consists of two steps. First, lemma @{text "\s \ s'; P s'; \ P s[; Q]\ \ R s'"} is +proven by simplification, using the definitions of protocol relations. Then, the target proposition +is proven by applying rule @{text rtrancl_start} as a destruction rule (cf. @{cite "Paulson20"}) and +proving @{term "P s'"} by assumption, @{term "\ P s"} by simplification, and the residual subgoal +by means of the previous lemma. + +In addition to the relational method, this paper is aimed at introducing still another enhancement: +besides message confidentiality and authenticity, it takes into consideration a further important +security property, \emph{message anonymity}. Being legitimate agents identified via natural numbers, +the fact that in state @{text s} the spy ignores that message @{text X\<^sub>n} is associated with agent +@{text n}, viz. @{text X\<^sub>n}'s property of being \emph{anonymous} in state @{text s}, can be expressed +as @{text "\n, X\<^sub>n\ \ spied s"}, where notation @{text "\n, X\<^sub>n\"} refers to a new constructor added to +datatype @{text msg} precisely for this purpose. + +A basic constraint upon any protocol relation augmenting the spy's knowledge with @{text "\n, X\"} +is that the spy must know message @{text X} in the current state, as it is impossible to identify +the agent associated with an unknown message. There is also an additional, more subtle constraint. +Any such protocol relation either augments a state in which the spy knows @{text "\n, C X\<^sub>1 \ X\<^sub>m\"}, +i.e. containing event @{text "(Spy, \n, C X\<^sub>1 \ X\<^sub>m\)"}, with event @{text "(Spy, \n, X\<^sub>i\)"}, where +$1 \leq i \leq m$ and @{text C} is some constructor of datatype @{text msg}, or conversely augments +a state containing event @{text "(Spy, \n, X\<^sub>i\)"} with @{text "(Spy, \n, C X\<^sub>1 \ X\<^sub>m\)"}. However, the +latter spy's inference is justified only if @{text "C X\<^sub>1 \ X\<^sub>m"} is part of a message generated or +accepted by some legitimate agent in accordance with the protocol rules. Otherwise, namely in case +@{text "C X\<^sub>1 \ X\<^sub>m"} were just a message generated at random by the spy, her inference would be as +sound as those of most politicians and all advertisements: even if the conclusion happened to be +true, it would be so by pure chance. + +This problem is solved as follows. + + \<^item> A further constructor @{text Log}, taking a message as input, is added to datatype @{text msg}, +and every protocol relation modeling the generation or acceptance of message @{text X} by some +legitimate agent must augment the current state with event @{term "(Spy, Log X)"}. +\\In this way, the set of all the messages having been exchanged by some legitimate agent in state +@{text s} can be expressed as @{term "Log -` spied s"}. + + \<^item> A function @{text crypts} is defined inductively. It takes a message set @{text H} as input, and +returns the least message set @{text H'} such that @{term "H \ H'"} and for any (even empty) list +of keys @{text KS}, if the encryption of @{text "\X, Y\"}, @{text "\Y, X\"}, or @{text "Hash X"} +with @{text KS} is included in @{text H'}, then the encryption of @{text X} with @{text KS} is +included in @{text H'} as well. +\\In this way, the set of all the messages exploitable in state @{text s} to map messages containing +them as components to agents can be expressed as @{term "crypts (Log -` spied s)"}. For instance, if +the encryption of @{text "Hash \X, Y\"} with key @{text K} lies within this set, then the encryption +of @{text X} with @{text K} also does, so that the spy can infer @{text "\n, Hash \X, Y\\"} from +@{text "\n, X\"} -- provided that she knows @{text Y} and @{text K}'s inverse key as well. + + \<^item> Another function @{text key_sets} is defined, too. It takes two inputs, a message @{text X} and +a message set @{text H}, and returns the set of the sets of @{text KS}' inverse keys for any list of +keys @{text KS} such that the encryption of @{text X} with @{text KS} is included in @{text H}. +\\In this way, the fact that in state @{text s} a message @{text X} can be exploited by the spy to +map a given message containing it as a component to an agent, provided that she knows all the keys +in set @{text U}, can be expressed via conditions @{term "U \ key_sets X (crypts (Log -` spied s))"} +and @{term "U \ spied s"}. +\\The choice to define @{text key_sets} so as to collect the inverse keys of encryption keys, viz. +decryption ones, depends on the fact that the sample protocol verified in this paper uses symmetric +keys alone -- which match their own inverse keys -- for encryption, whereas asymmetric key pairs are +used in cryptograms only for signature generation -- so that the inverse keys are public ones. In +case of a protocol (also) using public keys for encryption, encryption keys themselves should (also) +be collected, since the corresponding decryption keys, i.e. private keys, would be unknown to the +spy by default. This would formalize the fact that encrypted messages can be mapped to agents not +only by decrypting them, but also by recomputing the cryptograms (provided that the plaintexts are +known) and checking whether they match the exchanged ones. +\ + + +subsection "A sample protocol" + +text \ +As previously mentioned, this paper tries the relational method, including message anonymity, by +applying it to the verification of a sample authentication protocol in which Password Authenticated +Connection Establishment (PACE) with Chip Authentication Mapping (cf. @{cite "ICAO15"}) is first +used by an \emph{owner} to establish a secure channel with her own \emph{asset} and authenticate it, +and then the owner sends a password (other than the PACE one) to the asset over that channel so as +to authenticate herself. This enables to achieve a reliable mutual authentication even if the PACE +key is shared by multiple owners or is weak, as happens in electronic passports. Although the PACE +mechanism is specified for use in electronic documents, nothing prevents it in principle from being +used in other kinds of smart cards or even outside of the smart card world, which is the reason why +this paper uses the generic names \emph{asset} and \emph{owner} for the card and the cardholder, +respectively. + +In more detail, this protocol provides for the following steps. In this list, messages are specified +using the same syntax that will be adopted in the formal text (for further information about PACE +with Chip Authentication Mapping, cf. @{cite "ICAO15"}). + + \<^enum> \emph{Asset n} $\rightarrow$ \emph{Owner n}: +\\\hspace*{1em}@{text "Crypt (Auth_ShaKey n) (PriKey S)"} + + \<^enum> \emph{Owner n} $\rightarrow$ \emph{Asset n}: +\\\hspace*{1em}@{text "\Num 1, PubKey A\"} + + \<^enum> \emph{Asset n} $\rightarrow$ \emph{Owner n}: +\\\hspace*{1em}@{text "\Num 2, PubKey B\"} + + \<^enum> \emph{Owner n} $\rightarrow$ \emph{Asset n}: +\\\hspace*{1em}@{text "\Num 3, PubKey C\"} + + \<^enum> \emph{Asset n} $\rightarrow$ \emph{Owner n}: +\\\hspace*{1em}@{text "\Num 4, PubKey D\"} + + \<^enum> \emph{Owner n} $\rightarrow$ \emph{Asset n}: +\\\hspace*{1em}@{text "Crypt (SesK SK) (PubKey D)"} + + \<^enum> \emph{Asset n} $\rightarrow$ \emph{Owner n}: +\\\hspace*{1em}@{text "\Crypt (SesK SK) (PubKey C),"} +\\\hspace*{1.5em}@{text "Crypt (SesK SK) (Auth_PriK n \ B),"} +\\\hspace*{1.5em}@{text "Crypt (SesK SK) (Crypt SigK"} +\\\hspace*{2em}@{text "\Hash (Agent n), Hash (Auth_PubKey n)\)\"} + + \<^enum> \emph{Owner n} $\rightarrow$ \emph{Asset n}: +\\\hspace*{1em}@{text "Crypt (SesK SK) (Pwd n)"} + + \<^enum> \emph{Asset n} $\rightarrow$ \emph{Owner n}: +\\\hspace*{1em}@{text "Crypt (SesK SK) (Num 0)"} + +Legitimate agents consist of an infinite population of assets and owners. For each natural number +@{text n}, @{text "Owner n"} is an owner and @{text "Asset n"} is her own asset, and these agents +are assigned the following authentication data. + + \<^item> @{text "Key (Auth_ShaKey n)"}: static symmetric PACE key shared by both agents. + + \<^item> @{text "Auth_PriKey n"}, @{text "Auth_PubKey n"}: static private and public keys stored on +@{text "Asset n"} and used for @{text "Asset n"}'s authentication via Chip Authentication Mapping. + + \<^item> @{text "Pwd n"}: unique password (other than the PACE one) shared by both agents and used for +@{text "Owner n"}'s authentication. + +Function @{text Pwd} is defined as a constructor of datatype @{text msg} and then is injective, +which formalizes the assumption that each asset-owner pair has a distinct password, whereas no such +constraint is put on functions @{text Auth_ShaKey}, @{text Auth_PriKey}, and @{text Auth_PubKey}, +which allows multiple asset-owner pairs to be assigned the same keys. On the other hand, function +@{text Auth_PriKey} is constrained to be such that the complement of its range is infinite. As each +protocol run requires the generation of fresh ephemeral private keys, this constraint ensures that +an unbounded number of protocol runs can be carried out. All assumptions are formalized by applying +the definitional approach, viz. without introducing any axiom, and so is this constraint, expressed +by defining function @{text Auth_PriKey} using the indefinite description operator @{text SOME}. + +The protocol starts with @{text "Asset n"} sending an ephemeral private key encrypted with the PACE +key to @{text "Owner n"}. Actually, if @{text "Asset n"} is a smart card, the protocol should rather +start with @{text "Owner n"} sending a plain request for such encrypted nonce, but this preliminary +step is omitted here as it is irrelevant for protocol security. After that, @{text "Owner n"} and +@{text "Asset n"} generate two ephemeral key pairs each and send the respective public keys to the +other party. + +Then, both parties agree on the same session key by deriving it from the ephemeral keys generated +previously (actually, two distinct session keys would be derived, one for encryption and the other +one for MAC computation, but such a level of detail is unnecessary for protocol verification). The +session key is modeled as @{text "Key (SesK SK)"}, where @{text SesK} is an apposite constructor +added to datatype @{text key} and @{term "SK = (Some S, {A, B}, {C, D})"}. The adoption of type +@{typ "nat option"} for the first component enables to represent as @{term "(None, {A, B}, {C, D})"} +the wrong session key derived from @{text "Owner n"} if @{text "PriKey S"} was encrypted using a key +other than @{text "Key (Auth_ShaKey n)"} -- which reflects the fact that the protocol goes on even +without the two parties sharing the same session key. The use of type @{typ "nat set"} for the other +two components enables the spy to compute @{text "Key (SesK SK)"} if she knows \emph{either} private +key and the other public key referenced by each set, as long as she also knows @{text "PriKey S"} -- +which reflects the fact that given two key pairs, Diffie-Hellman key agreement generates the same +shared secret independently of which of the respective private keys is used for computation. + +This session key is used by both parties to compute their authentication tokens. Both encrypt the +other party's second ephemeral public key, but @{text "Asset n"} appends two further fields: the +Encrypted Chip Authentication Data, as provided for by Chip Authentication Mapping, and an encrypted +signature of the hash values of @{text "Agent n"} and @{text "Auth_PubKey n"}. Infix notation +@{text "Auth_PriK n \ B"} refers to a constructor of datatype @{text msg} standing for plain Chip +Authentication Data, and @{text Agent} is another such constructor standing for agent identification +data. @{text "Owner n"} is expected to validate this signature by also checking @{text "Agent n"}'s +hash value against reference identification data known by other means -- otherwise, the spy would +not be forced to know @{text "Auth_PriKey n"} to masquerade as @{text "Asset n"}, since she could do +that by just knowing @{text "Auth_PriKey m"} for some other @{text m}, even if @{term "Auth_PriKey m +\ Auth_PriKey n"}. If @{text "Asset n"} is an electronic passport, the owner, i.e. the inspection +system, could get cardholder's identification data by reading her personal data on the booklet, and +such a signature could be retrieved from the chip (actually through a distinct message, but this is +irrelevant for protocol security as long as the password is sent after the signature's validation) +by reading the Document Security Object -- provided that @{text "Auth_PubKey n"} is included within +Data Group 14. + +The protocol ends with @{text "Owner n"} sending her password, encrypted with the session key, to +@{text "Asset n"}, who validates it and replies with an encrypted acknowledgment. + +Here below are some concluding remarks about the way how this sample protocol is formalized. + + \<^item> A single signature private key, unknown to the spy, is assumed to be used for all legitimate +agents. Similarly, the spy might have hacked some legitimate agent so as to steal her ephemeral +private keys as soon as they are generated, but here all legitimate agents are assumed to be out of +the spy's reach in this respect. Of course, this is just the choice of one of multiple possible +scenarios, and nothing prevents these assumptions from being dropped. + + \<^item> In the real world, a legitimate agent would use any one of her ephemeral private keys just once, +after which the key would be destroyed. On the contrary, no such constraint is enforced here, since +it turns out to be unnecessary for protocol verification. There is a single exception, required for +the proof of a unicity lemma: after @{text "Asset n"} has used @{text "PriKey B"} to compute her +authentication token, she must discard @{text "PriKey B"} so as not to use this key any longer. The +way how this requirement is expressed emphasizes once more the flexibility of the modeling of events +in the relational method: @{text "Asset n"} may use @{text "PriKey B"} in this computation only if +event @{text "(Asset n, PubKey B)"} is not yet contained in the current state @{text s}, and then +@{text s} is augmented with that event. Namely, events can also be used to model garbage collection! + + \<^item> The protocol rules augmenting the spy's knowledge with some message of the form @{text "\n, X\"} +generally require the spy to already know some other message of the same form. There is just one +exception: the spy can infer @{text "\n, Agent n\"} from @{text "Agent n"}. This expresses the fact +that the detection of identification data within a message generated or accepted by a legitimate +agent is itself sufficient to map any known component of that message to that agent, regardless of +whether any data were already mapped to that agent in advance. + +The formal content is split into the following sections. + + \<^item> Section \ref{Definitions}, \emph{Definitions}, contains all the definitions needed to formalize +the sample protocol by means of the relational method, including message anonymity. + + \<^item> Section \ref{Authentication}, \emph{Confidentiality and authenticity properties}, proves that +the following theorems hold under appropriate assumptions. + + \<^enum> Theorem @{text sigkey_secret}: the signature private key is secret. + + \<^enum> Theorem @{text auth_shakey_secret}: an asset-owner pair's PACE key is secret. + + \<^enum> Theorem @{text auth_prikey_secret}: an asset's Chip Authentication private key is secret. + + \<^enum> Theorem @{text owner_seskey_unique}: an owner's session key is unknown to other owners. + + \<^enum> Theorem @{text owner_seskey_secret}: an owner's session key is secret. + + \<^enum> Theorem @{text owner_num_genuine}: the encrypted acknowledgment received by an owner has been +sent by the respective asset. + + \<^enum> Theorem @{text owner_token_genuine}: the PACE authentication token received by an owner has +been generated by the respective asset, using her Chip Authentication private key and the same +ephemeral keys used to derive the session key. + + \<^enum> Theorem @{text pwd_secret}: an asset-owner pair's password is secret. + + \<^enum> Theorem @{text asset_seskey_unique}: an asset's session key is unknown to other assets, and +may be used by that asset to compute just one PACE authentication token. + + \<^enum> Theorem @{text asset_seskey_secret}: an asset's session key is secret. + + \<^enum> Theorem @{text asset_pwd_genuine}: the encrypted password received by an asset has been sent +by the respective owner. + + \<^enum> Theorem @{text asset_token_genuine}: the PACE authentication token received by an asset has +been generated by the respective owner, using the same ephemeral key used to derive the session key. + + Particularly, these proofs confirm that the mutual authentication between an owner and her asset +is reliable even if their PACE key is compromised, unless either their Chip Authentication private +key or their password also is -- namely, the protocol succeeds in implementing a two-factor mutual +authentication. + + \<^item> Section \ref{Anonymity}, \emph{Anonymity properties}, proves that the following theorems hold +under appropriate assumptions. + + \<^enum> Theorem @{text pwd_anonymous}: an asset-owner pair's password is anonymous. + + \<^enum> Theorem @{text auth_prikey_anonymous}: an asset's Chip Authentication private key is +anonymous. + + \<^enum> Theorem @{text auth_shakey_anonymous}: an asset-owner pair's PACE key is anonymous. + + \<^item> Section \ref{Possibility}, \emph{Possibility properties}, shows how possibility properties (cf. +@{cite "Paulson98"}) can be proven by constructing sample protocol runs, either ordinary or attack +ones. Two such properties are proven: + + \<^enum> Theorem @{text runs_unbounded}: for any possible protocol state @{text s} and any asset-owner +pair, there exists a state @{text s'} reachable from @{text s} in which a protocol run has been +completed by those agents using an ephemeral private key @{text "PriKey S"} not yet exchanged in +@{text s} -- namely, an unbounded number of protocol runs can be carried out by legitimate agents. + + \<^enum> Theorem @{text pwd_compromised}: in a scenario not satisfying the assumptions of theorem +@{text pwd_anonymous}, the spy can steal an asset-owner pair's password and even identify those +agents. + + The latter is an example of a possibility property aimed at confirming that the assumptions of a +given confidentiality, authenticity, or anonymity property are necessary for it to hold. + +For further information about the formal definitions and proofs contained in these sections, see +Isabelle documentation, particularly @{cite "Paulson20"}, @{cite "Nipkow20"}, @{cite "Krauss20"}, +and @{cite "Nipkow11"}. + +\textbf{Important note.} This sample protocol was already considered in a former paper of mine (cf. +@{cite "Noce17"}). For any purpose, that paper should be regarded as being obsolete and superseded +by the present paper. +\ + + +subsection "Definitions" + +text \ +\label{Definitions} +\ + +type_synonym agent_id = nat + +type_synonym key_id = nat + +type_synonym seskey_in = "key_id option \ key_id set \ key_id set" + +datatype agent = + Asset agent_id | + Owner agent_id | + Spy + +datatype key = + SigK | + VerK | + PriK key_id | + PubK key_id | + ShaK key_id | + SesK seskey_in + +datatype msg = + Num nat | + Agent agent_id | + Pwd agent_id | + Key key | + Mult key_id key_id (infixl "\" 70) | + Hash msg | + Crypt key msg | + MPair msg msg | + IDInfo agent_id msg | + Log msg + +syntax + "_MPair" :: "['a, args] \ 'a * 'b" ("(2\_,/ _\)") + "_IDInfo" :: "[agent_id, msg] \ msg" ("(2\_,/ _\)") +translations + "\X, Y, Z\" \ "\X, \Y, Z\\" + "\X, Y\" \ "CONST MPair X Y" + "\n, X\" \ "CONST IDInfo n X" + + +abbreviation SigKey :: "msg" where +"SigKey \ Key SigK" + +abbreviation VerKey :: "msg" where +"VerKey \ Key VerK" + +abbreviation PriKey :: "key_id \ msg" where +"PriKey \ Key \ PriK" + +abbreviation PubKey :: "key_id \ msg" where +"PubKey \ Key \ PubK" + +abbreviation ShaKey :: "key_id \ msg" where +"ShaKey \ Key \ ShaK" + +abbreviation SesKey :: "seskey_in \ msg" where +"SesKey \ Key \ SesK" + +primrec InvK :: "key \ key" where +"InvK SigK = VerK" | +"InvK VerK = SigK" | +"InvK (PriK A) = PubK A" | +"InvK (PubK A) = PriK A" | +"InvK (ShaK SK) = ShaK SK" | +"InvK (SesK SK) = SesK SK" + +abbreviation InvKey :: "key \ msg" where +"InvKey \ Key \ InvK" + + +inductive_set parts :: "msg set \ msg set" + for H :: "msg set" where + +parts_used [intro]: + "X \ H \ X \ parts H" | + +parts_crypt [intro]: + "Crypt K X \ parts H \ X \ parts H" | + +parts_fst [intro]: + "\X, Y\ \ parts H \ X \ parts H" | + +parts_snd [intro]: + "\X, Y\ \ parts H \ Y \ parts H" + + +inductive_set crypts :: "msg set \ msg set" + for H :: "msg set" where + +crypts_used [intro]: + "X \ H \ X \ crypts H" | + +crypts_hash [intro]: + "foldr Crypt KS (Hash X) \ crypts H \ foldr Crypt KS X \ crypts H" | + +crypts_fst [intro]: + "foldr Crypt KS \X, Y\ \ crypts H \ foldr Crypt KS X \ crypts H" | + +crypts_snd [intro]: + "foldr Crypt KS \X, Y\ \ crypts H \ foldr Crypt KS Y \ crypts H" + + +definition key_sets :: "msg \ msg set \ msg set set" where +"key_sets X H \ {InvKey ` set KS | KS. foldr Crypt KS X \ H}" + +definition parts_msg :: "msg \ msg set" where +"parts_msg X \ parts {X}" + +definition crypts_msg :: "msg \ msg set" where +"crypts_msg X \ crypts {X}" + +definition key_sets_msg :: "msg \ msg \ msg set set" where +"key_sets_msg X Y \ key_sets X {Y}" + +fun seskey_set :: "seskey_in \ key_id set" where +"seskey_set (Some S, U, V) = insert S (U \ V)" | +"seskey_set (None, U, V) = U \ V" + + +definition Auth_PriK :: "agent_id \ key_id" where +"Auth_PriK \ SOME f. infinite (- range f)" + +abbreviation Auth_PriKey :: "agent_id \ msg" where +"Auth_PriKey \ PriKey \ Auth_PriK" + +abbreviation Auth_PubKey :: "agent_id \ msg" where +"Auth_PubKey \ PubKey \ Auth_PriK" + +consts Auth_ShaK :: "agent_id \ key_id" + +abbreviation Auth_ShaKey :: "agent_id \ key" where +"Auth_ShaKey \ ShaK \ Auth_ShaK" + +abbreviation Sign :: "agent_id \ key_id \ msg" where +"Sign n A \ Crypt SigK \Hash (Agent n), Hash (PubKey A)\" + +abbreviation Token :: "agent_id \ key_id \ key_id \ key_id \ seskey_in \ msg" +where "Token n A B C SK \ \Crypt (SesK SK) (PubKey C), + Crypt (SesK SK) (A \ B), Crypt (SesK SK) (Sign n A)\" + + +consts bad_agent :: "agent_id set" + +consts bad_pwd :: "agent_id set" + +consts bad_shak :: "key_id set" + +consts bad_id_pwd :: "agent_id set" + +consts bad_id_prik :: "agent_id set" + +consts bad_id_pubk :: "agent_id set" + +consts bad_id_shak :: "agent_id set" + +definition bad_prik :: "key_id set" where +"bad_prik \ SOME U. U \ range Auth_PriK" + +abbreviation bad_prikey :: "agent_id set" where +"bad_prikey \ Auth_PriK -` bad_prik" + +abbreviation bad_shakey :: "agent_id set" where +"bad_shakey \ Auth_ShaK -` bad_shak" + +abbreviation bad_id_password :: "agent_id set" where +"bad_id_password \ bad_id_pwd \ bad_pwd" + +abbreviation bad_id_prikey :: "agent_id set" where +"bad_id_prikey \ (bad_agent \ bad_id_pubk \ bad_id_prik) \ bad_prikey" + +abbreviation bad_id_pubkey :: "agent_id set" where +"bad_id_pubkey \ bad_agent \ bad_id_pubk \ bad_id_prik \ bad_prikey" + +abbreviation bad_id_shakey :: "agent_id set" where +"bad_id_shakey \ bad_id_shak \ bad_shakey" + + +type_synonym event = "agent \ msg" + +type_synonym state = "event set" + +abbreviation used :: "state \ msg set" where +"used s \ Range s" + +abbreviation spied :: "state \ msg set" where +"spied s \ s `` {Spy}" + +abbreviation s\<^sub>0 :: state where +"s\<^sub>0 \ range (\n. (Asset n, Auth_PriKey n)) \ {Spy} \ insert VerKey + (range Num \ range Auth_PubKey \ range (\n. Sign n (Auth_PriK n)) \ + Agent ` bad_agent \ Pwd ` bad_pwd \ PriKey ` bad_prik \ ShaKey ` bad_shak \ + (\n. \n, Pwd n\) ` bad_id_password \ + (\n. \n, Auth_PriKey n\) ` bad_id_prikey \ + (\n. \n, Auth_PubKey n\) ` bad_id_pubkey \ + (\n. \n, Key (Auth_ShaKey n)\) ` bad_id_shakey)" + + +abbreviation rel_asset_i :: "(state \ state) set" where +"rel_asset_i \ {(s, s') | s s' n S. + s' = insert (Asset n, PriKey S) s \ + {Asset n, Spy} \ {Crypt (Auth_ShaKey n) (PriKey S)} \ + {(Spy, Log (Crypt (Auth_ShaKey n) (PriKey S)))} \ + PriKey S \ used s}" + +abbreviation rel_owner_ii :: "(state \ state) set" where +"rel_owner_ii \ {(s, s') | s s' n S A K. + s' = insert (Owner n, PriKey A) s \ + {Owner n, Spy} \ {\Num 1, PubKey A\} \ + {Spy} \ Log ` {Crypt K (PriKey S), \Num 1, PubKey A\} \ + Crypt K (PriKey S) \ used s \ + PriKey A \ used s}" + +abbreviation rel_asset_ii :: "(state \ state) set" where +"rel_asset_ii \ {(s, s') | s s' n A B. + s' = insert (Asset n, PriKey B) s \ + {Asset n, Spy} \ {\Num 2, PubKey B\} \ + {Spy} \ Log ` {\Num 1, PubKey A\, \Num 2, PubKey B\} \ + \Num 1, PubKey A\ \ used s \ + PriKey B \ used s}" + +abbreviation rel_owner_iii :: "(state \ state) set" where +"rel_owner_iii \ {(s, s') | s s' n B C. + s' = insert (Owner n, PriKey C) s \ + {Owner n, Spy} \ {\Num 3, PubKey C\} \ + {Spy} \ Log ` {\Num 2, PubKey B\, \Num 3, PubKey C\} \ + \Num 2, PubKey B\ \ used s \ + PriKey C \ used s}" + +abbreviation rel_asset_iii :: "(state \ state) set" where +"rel_asset_iii \ {(s, s') | s s' n C D. + s' = insert (Asset n, PriKey D) s \ + {Asset n, Spy} \ {\Num 4, PubKey D\} \ + {Spy} \ Log ` {\Num 3, PubKey C\, \Num 4, PubKey D\} \ + \Num 3, PubKey C\ \ used s \ + PriKey D \ used s}" + +abbreviation rel_owner_iv :: "(state \ state) set" where +"rel_owner_iv \ {(s, s') | s s' n S A B C D K SK. + s' = insert (Owner n, SesKey SK) s \ + {Owner n, Spy} \ {Crypt (SesK SK) (PubKey D)} \ + {Spy} \ Log ` {\Num 4, PubKey D\, Crypt (SesK SK) (PubKey D)} \ + {Crypt K (PriKey S), \Num 2, PubKey B\, \Num 4, PubKey D\} \ used s \ + {Owner n} \ {\Num 1, PubKey A\, \Num 3, PubKey C\} \ s \ + SK = (if K = Auth_ShaKey n then Some S else None, {A, B}, {C, D})}" + +abbreviation rel_asset_iv :: "(state \ state) set" where +"rel_asset_iv \ {(s, s') | s s' n S A B C D SK. + s' = s \ {Asset n} \ {SesKey SK, PubKey B} \ + {Asset n, Spy} \ {Token n (Auth_PriK n) B C SK} \ + {Spy} \ Log ` {Crypt (SesK SK) (PubKey D), + Token n (Auth_PriK n) B C SK} \ + {Asset n} \ {Crypt (Auth_ShaKey n) (PriKey S), + \Num 2, PubKey B\, \Num 4, PubKey D\} \ s \ + {\Num 1, PubKey A\, \Num 3, PubKey C\, + Crypt (SesK SK) (PubKey D)} \ used s \ + (Asset n, PubKey B) \ s \ + SK = (Some S, {A, B}, {C, D})}" + +abbreviation rel_owner_v :: "(state \ state) set" where +"rel_owner_v \ {(s, s') | s s' n A B C SK. + s' = s \ {Owner n, Spy} \ {Crypt (SesK SK) (Pwd n)} \ + {Spy} \ Log ` {Token n A B C SK, Crypt (SesK SK) (Pwd n)} \ + Token n A B C SK \ used s \ + (Owner n, SesKey SK) \ s \ + B \ fst (snd SK)}" + +abbreviation rel_asset_v :: "(state \ state) set" where +"rel_asset_v \ {(s, s') | s s' n SK. + s' = s \ {Asset n, Spy} \ {Crypt (SesK SK) (Num 0)} \ + {Spy} \ Log ` {Crypt (SesK SK) (Pwd n), Crypt (SesK SK) (Num 0)} \ + (Asset n, SesKey SK) \ s \ + Crypt (SesK SK) (Pwd n) \ used s}" + + +abbreviation rel_prik :: "(state \ state) set" where +"rel_prik \ {(s, s') | s s' A. + s' = insert (Spy, PriKey A) s \ + PriKey A \ used s}" + +abbreviation rel_pubk :: "(state \ state) set" where +"rel_pubk \ {(s, s') | s s' A. + s' = insert (Spy, PubKey A) s \ + PriKey A \ spied s}" + +abbreviation rel_sesk :: "(state \ state) set" where +"rel_sesk \ {(s, s') | s s' A B C D S. + s' = insert (Spy, SesKey (Some S, {A, B}, {C, D})) s \ + {PriKey S, PriKey A, PubKey B, PriKey C, PubKey D} \ spied s}" + +abbreviation rel_fact :: "(state \ state) set" where +"rel_fact \ {(s, s') | s s' A B. + s' = s \ {Spy} \ {PriKey A, PriKey B} \ + A \ B \ spied s \ + (PriKey A \ spied s \ PriKey B \ spied s)}" + +abbreviation rel_mult :: "(state \ state) set" where +"rel_mult \ {(s, s') | s s' A B. + s' = insert (Spy, A \ B) s \ + {PriKey A, PriKey B} \ spied s}" + +abbreviation rel_hash :: "(state \ state) set" where +"rel_hash \ {(s, s') | s s' X. + s' = insert (Spy, Hash X) s \ + X \ spied s}" + +abbreviation rel_dec :: "(state \ state) set" where +"rel_dec \ {(s, s') | s s' K X. + s' = insert (Spy, X) s \ + {Crypt K X, InvKey K} \ spied s}" + +abbreviation rel_enc :: "(state \ state) set" where +"rel_enc \ {(s, s') | s s' K X. + s' = insert (Spy, Crypt K X) s \ + {X, Key K} \ spied s}" + +abbreviation rel_sep :: "(state \ state) set" where +"rel_sep \ {(s, s') | s s' X Y. + s' = s \ {Spy} \ {X, Y} \ + \X, Y\ \ spied s}" + +abbreviation rel_con :: "(state \ state) set" where +"rel_con \ {(s, s') | s s' X Y. + s' = insert (Spy, \X, Y\) s \ + {X, Y} \ spied s}" + + +abbreviation rel_id_agent :: "(state \ state) set" where +"rel_id_agent \ {(s, s') | s s' n. + s' = insert (Spy, \n, Agent n\) s \ + Agent n \ spied s}" + +abbreviation rel_id_invk :: "(state \ state) set" where +"rel_id_invk \ {(s, s') | s s' n K. + s' = insert (Spy, \n, InvKey K\) s \ + {InvKey K, \n, Key K\} \ spied s}" + +abbreviation rel_id_sesk :: "(state \ state) set" where +"rel_id_sesk \ {(s, s') | s s' n A SK X U. + s' = s \ {Spy} \ {\n, PubKey A\, \n, SesKey SK\} \ + {PubKey A, SesKey SK} \ spied s \ + (\n, PubKey A\ \ spied s \ \n, SesKey SK\ \ spied s) \ + A \ seskey_set SK \ + SesKey SK \ U \ + U \ key_sets X (crypts (Log -` spied s))}" + +abbreviation rel_id_fact :: "(state \ state) set" where +"rel_id_fact \ {(s, s') | s s' n A B. + s' = s \ {Spy} \ {\n, PriKey A\, \n, PriKey B\} \ + {PriKey A, PriKey B, \n, A \ B\} \ spied s}" + +abbreviation rel_id_mult :: "(state \ state) set" where +"rel_id_mult \ {(s, s') | s s' n A B U. + s' = insert (Spy, \n, A \ B\) s \ + U \ {PriKey A, PriKey B, A \ B} \ spied s \ + (\n, PriKey A\ \ spied s \ \n, PriKey B\ \ spied s) \ + U \ key_sets (A \ B) (crypts (Log -` spied s))}" + +abbreviation rel_id_hash :: "(state \ state) set" where +"rel_id_hash \ {(s, s') | s s' n X U. + s' = s \ {Spy} \ {\n, X\, \n, Hash X\} \ + U \ {X, Hash X} \ spied s \ + (\n, X\ \ spied s \ \n, Hash X\ \ spied s) \ + U \ key_sets (Hash X) (crypts (Log -` spied s))}" + +abbreviation rel_id_crypt :: "(state \ state) set" where +"rel_id_crypt \ {(s, s') | s s' n X U. + s' = s \ {Spy} \ IDInfo n ` insert X U \ + insert X U \ spied s \ + (\n, X\ \ spied s \ (\K \ U. \n, K\ \ spied s)) \ + U \ key_sets X (crypts (Log -` spied s))}" + +abbreviation rel_id_sep :: "(state \ state) set" where +"rel_id_sep \ {(s, s') | s s' n X Y. + s' = s \ {Spy} \ {\n, X\, \n, Y\} \ + {X, Y, \n, \X, Y\\} \ spied s}" + +abbreviation rel_id_con :: "(state \ state) set" where +"rel_id_con \ {(s, s') | s s' n X Y U. + s' = insert (Spy, \n, \X, Y\\) s \ + U \ {X, Y, \X, Y\} \ spied s \ + (\n, X\ \ spied s \ \n, Y\ \ spied s) \ + U \ key_sets \X, Y\ (crypts (Log -` spied s))}" + + +definition rel :: "(state \ state) set" where +"rel \ rel_asset_i \ rel_owner_ii \ rel_asset_ii \ rel_owner_iii \ + rel_asset_iii \ rel_owner_iv \ rel_asset_iv \ rel_owner_v \ rel_asset_v \ + rel_prik \ rel_pubk \ rel_sesk \ rel_fact \ rel_mult \ rel_hash \ rel_dec \ + rel_enc \ rel_sep \ rel_con \ rel_id_agent \ rel_id_invk \ rel_id_sesk \ + rel_id_fact \ rel_id_mult \ rel_id_hash \ rel_id_crypt \ rel_id_sep \ rel_id_con" + +abbreviation in_rel :: "state \ state \ bool" (infix "\" 60) where +"s \ s' \ (s, s') \ rel" + +abbreviation in_rel_rtrancl :: "state \ state \ bool" (infix "\" 60) where +"s \ s' \ (s, s') \ rel\<^sup>*" + + +end diff --git a/thys/Relational_Method/Possibility.thy b/thys/Relational_Method/Possibility.thy new file mode 100644 --- /dev/null +++ b/thys/Relational_Method/Possibility.thy @@ -0,0 +1,990 @@ +(* Title: The Relational Method with Message Anonymity for the Verification of Cryptographic Protocols + Author: Pasquale Noce + Software Engineer at HID Global, Italy + pasquale dot noce dot lavoro at gmail dot com + pasquale dot noce at hidglobal dot com +*) + +section "Possibility properties" + +theory Possibility + imports Anonymity +begin + +text \ +\label{Possibility} +\ + + +type_synonym seskey_tuple = "key_id \ key_id \ key_id \ key_id \ key_id" + +type_synonym stage = "state \ seskey_tuple" + + +abbreviation pred_asset_i :: "agent_id \ state \ stage \ bool" where +"pred_asset_i n s x \ + \S. PriKey S \ used s \ x = (insert (Asset n, PriKey S) s \ + {Asset n, Spy} \ {Crypt (Auth_ShaKey n) (PriKey S)} \ + {(Spy, Log (Crypt (Auth_ShaKey n) (PriKey S)))}, + S, 0, 0, 0, 0)" + +definition run_asset_i :: "agent_id \ state \ stage" where +"run_asset_i n s \ SOME x. pred_asset_i n s x" + + +abbreviation pred_owner_ii :: "agent_id \ stage \ stage \ bool" where +"pred_owner_ii n x y \ case x of (s, S, _) \ + \A. PriKey A \ used s \ y = (insert (Owner n, PriKey A) s \ + {Owner n, Spy} \ {\Num 1, PubKey A\} \ + {Spy} \ Log ` {Crypt (Auth_ShaKey n) (PriKey S), \Num 1, PubKey A\}, + S, A, 0, 0, 0)" + +definition run_owner_ii :: "agent_id \ state \ stage" where +"run_owner_ii n s \ SOME x. pred_owner_ii n (run_asset_i n s) x" + + +abbreviation pred_asset_ii :: "agent_id \ stage \ stage \ bool" where +"pred_asset_ii n x y \ case x of (s, S, A, _) \ + \B. PriKey B \ used s \ y = (insert (Asset n, PriKey B) s \ + {Asset n, Spy} \ {\Num 2, PubKey B\} \ + {Spy} \ Log ` {\Num 1, PubKey A\, \Num 2, PubKey B\}, + S, A, B, 0, 0)" + +definition run_asset_ii :: "agent_id \ state \ stage" where +"run_asset_ii n s \ SOME x. pred_asset_ii n (run_owner_ii n s) x" + + +abbreviation pred_owner_iii :: "agent_id \ stage \ stage \ bool" where +"pred_owner_iii n x y \ case x of (s, S, A, B, _) \ + \C. PriKey C \ used s \ y = (insert (Owner n, PriKey C) s \ + {Owner n, Spy} \ {\Num 3, PubKey C\} \ + {Spy} \ Log ` {\Num 2, PubKey B\, \Num 3, PubKey C\}, + S, A, B, C, 0)" + +definition run_owner_iii :: "agent_id \ state \ stage" where +"run_owner_iii n s \ SOME x. pred_owner_iii n (run_asset_ii n s) x" + + +abbreviation pred_asset_iii :: "agent_id \ stage \ stage \ bool" where +"pred_asset_iii n x y \ case x of (s, S, A, B, C, _) \ + \D. PriKey D \ used s \ y = (insert (Asset n, PriKey D) s \ + {Asset n, Spy} \ {\Num 4, PubKey D\} \ + {Spy} \ Log ` {\Num 3, PubKey C\, \Num 4, PubKey D\}, + S, A, B, C, D)" + +definition run_asset_iii :: "agent_id \ state \ stage" where +"run_asset_iii n s \ SOME x. pred_asset_iii n (run_owner_iii n s) x" + + +abbreviation stage_owner_iv :: "agent_id \ stage \ stage" where +"stage_owner_iv n x \ let (s, S, A, B, C, D) = x; + SK = (Some S, {A, B}, {C, D}) in + (insert (Owner n, SesKey SK) s \ + {Owner n, Spy} \ {Crypt (SesK SK) (PubKey D)} \ + {Spy} \ Log ` {\Num 4, PubKey D\, Crypt (SesK SK) (PubKey D)}, + S, A, B, C, D)" + +definition run_owner_iv :: "agent_id \ state \ stage" where +"run_owner_iv n s \ stage_owner_iv n (run_asset_iii n s)" + + +abbreviation stage_asset_iv :: "agent_id \ stage \ stage" where +"stage_asset_iv n x \ let (s, S, A, B, C, D) = x; + SK = (Some S, {A, B}, {C, D}) in + (s \ {Asset n} \ {SesKey SK, PubKey B} \ + {Asset n, Spy} \ {Token n (Auth_PriK n) B C SK} \ + {Spy} \ Log ` {Crypt (SesK SK) (PubKey D), + Token n (Auth_PriK n) B C SK}, + S, A, B, C, D)" + +definition run_asset_iv :: "agent_id \ state \ stage" where +"run_asset_iv n s \ stage_asset_iv n (run_owner_iv n s)" + + +abbreviation stage_owner_v :: "agent_id \ stage \ stage" where +"stage_owner_v n x \ let (s, S, A, B, C, D) = x; + SK = (Some S, {A, B}, {C, D}) in + (s \ {Owner n, Spy} \ {Crypt (SesK SK) (Pwd n)} \ + {Spy} \ Log ` {Token n (Auth_PriK n) B C SK, Crypt (SesK SK) (Pwd n)}, + S, A, B, C, D)" + +definition run_owner_v :: "agent_id \ state \ stage" where +"run_owner_v n s \ stage_owner_v n (run_asset_iv n s)" + + +abbreviation stage_asset_v :: "agent_id \ stage \ stage" where +"stage_asset_v n x \ let (s, S, A, B, C, D) = x; + SK = (Some S, {A, B}, {C, D}) in + (s \ {Asset n, Spy} \ {Crypt (SesK SK) (Num 0)} \ + {Spy} \ Log ` {Crypt (SesK SK) (Pwd n), Crypt (SesK SK) (Num 0)}, + S, A, B, C, D)" + +definition run_asset_v :: "agent_id \ state \ stage" where +"run_asset_v n s \ stage_asset_v n (run_owner_v n s)" + + +lemma prikey_unused_1: + "infinite {A. PriKey A \ used s\<^sub>0}" +by (rule infinite_super [of "- range Auth_PriK"], rule subsetI, simp add: + image_def bad_prik_def, rule someI2 [of _ "{}"], simp, blast, subst Auth_PriK_def, + rule someI [of _ "\n. 0"], simp) + +lemma prikey_unused_2: + "\s \ s'; infinite {A. PriKey A \ used s}\ \ + infinite {A. PriKey A \ used s'}" +by (simp add: rel_def, ((erule disjE)?, (erule exE)+, simp add: image_iff, + (((subst conj_commute | subst Int_commute), simp add: Collect_conj_eq Collect_neg_eq + Diff_eq [symmetric])+)?, ((rule Diff_infinite_finite, rule msg.induct, simp_all, + rule key.induct, simp_all)+)?)+) + +proposition prikey_unused: + "s\<^sub>0 \ s \ \A. PriKey A \ used s" +by (subgoal_tac "infinite {A. PriKey A \ used s}", drule infinite_imp_nonempty, + simp, erule rtrancl_induct, rule prikey_unused_1, rule prikey_unused_2) + + +lemma pubkey_unused_1: + "\s \ s'; PubKey A \ parts (used s) \ PriKey A \ used s; + PubKey A \ parts (used s')\ \ + PriKey A \ used s'" +by (simp add: rel_def, ((erule disjE)?, ((erule exE)+)?, simp add: parts_insert + image_iff split: if_split_asm, ((erule conjE)+, drule RangeI, (drule parts_used, + drule parts_snd)?, simp | (subst (asm) disj_assoc [symmetric])?, erule disjE, + (drule parts_dec | drule parts_enc | drule parts_sep | drule parts_con), simp)?)+) + +proposition pubkey_unused [rule_format]: + "s\<^sub>0 \ s \ + PriKey A \ used s \ + PubKey A \ parts (used s)" +by (erule rtrancl_induct, subst parts_init, simp add: Range_iff image_def, rule impI, + erule contrapos_nn [OF _ pubkey_unused_1], blast+) + + +proposition run_asset_i_ex: + "s\<^sub>0 \ s \ pred_asset_i n s (run_asset_i n s)" +by (drule prikey_unused, erule exE, subst run_asset_i_def, rule someI_ex, blast) + +proposition run_asset_i_rel: + "s\<^sub>0 \ s \ s \ fst (run_asset_i n s)" + (is "_ \ _ \ ?t") +by (drule run_asset_i_ex [of _ n], rule r_into_rtrancl, + subgoal_tac "(s, ?t) \ rel_asset_i", simp_all add: rel_def, erule exE, auto) + +proposition run_asset_i_msg: + "s\<^sub>0 \ s \ + case run_asset_i n s of (s', S, _) \ + (Asset n, Crypt (Auth_ShaKey n) (PriKey S)) \ s'" +by (drule run_asset_i_ex [of _ n], auto) + +proposition run_asset_i_nonce: + "s\<^sub>0 \ s \ PriKey (fst (snd (run_asset_i n s))) \ used s" +by (drule run_asset_i_ex [of _ n], auto) + +proposition run_asset_i_unused: + "s\<^sub>0 \ s \ \A. PriKey A \ used (fst (run_asset_i n s))" +by (rule prikey_unused, rule rtrancl_trans, simp, rule run_asset_i_rel) + + +proposition run_owner_ii_ex: + "s\<^sub>0 \ s \ pred_owner_ii n (run_asset_i n s) (run_owner_ii n s)" +by (drule run_asset_i_unused, erule exE, subst run_owner_ii_def, rule someI_ex, + auto simp add: split_def) + +proposition run_owner_ii_rel: + "s\<^sub>0 \ s \ s \ fst (run_owner_ii n s)" + (is "_ \ _ \ ?t") +by (rule rtrancl_into_rtrancl, erule run_asset_i_rel [of _ n], frule run_asset_i_msg, + drule run_owner_ii_ex, subgoal_tac "(fst (run_asset_i n s), ?t) \ rel_owner_ii", + simp_all add: rel_def split_def, erule exE, (rule exI)+, auto) + +proposition run_owner_ii_msg: + "s\<^sub>0 \ s \ + case run_owner_ii n s of (s', S, A, _) \ + {(Asset n, Crypt (Auth_ShaKey n) (PriKey S)), + (Owner n, \Num 1, PubKey A\)} \ s'" +by (frule run_asset_i_msg [of _ n], drule run_owner_ii_ex [of _ n], auto) + +proposition run_owner_ii_nonce: + "s\<^sub>0 \ s \ PriKey (fst (snd (run_owner_ii n s))) \ used s" +by (frule run_asset_i_nonce [of _ n], drule run_owner_ii_ex [of _ n], auto) + +proposition run_owner_ii_unused: + "s\<^sub>0 \ s \ \B. PriKey B \ used (fst (run_owner_ii n s))" +by (rule prikey_unused, rule rtrancl_trans, simp, rule run_owner_ii_rel) + + +proposition run_asset_ii_ex: + "s\<^sub>0 \ s \ pred_asset_ii n (run_owner_ii n s) (run_asset_ii n s)" +by (drule run_owner_ii_unused, erule exE, subst run_asset_ii_def, rule someI_ex, + auto simp add: split_def) + +proposition run_asset_ii_rel: + "s\<^sub>0 \ s \ s \ fst (run_asset_ii n s)" + (is "_ \ _ \ ?t") +by (rule rtrancl_into_rtrancl, erule run_owner_ii_rel [of _ n], frule run_owner_ii_msg, + drule run_asset_ii_ex, subgoal_tac "(fst (run_owner_ii n s), ?t) \ rel_asset_ii", + simp_all add: rel_def split_def, erule exE, (rule exI)+, auto) + +proposition run_asset_ii_msg: + assumes A: "s\<^sub>0 \ s" + shows "case run_asset_ii n s of (s', S, A, B, _) \ + insert (Owner n, \Num 1, PubKey A\) + ({Asset n} \ {Crypt (Auth_ShaKey n) (PriKey S), + \Num 2, PubKey B\}) \ s' \ + (Asset n, PubKey B) \ s'" +by (insert run_owner_ii_msg [OF A, of n], insert run_asset_ii_ex [OF A, of n], + simp add: split_def, erule exE, simp, insert run_owner_ii_rel [OF A, of n], + drule rtrancl_trans [OF A], drule pubkey_unused, auto) + +proposition run_asset_ii_nonce: + "s\<^sub>0 \ s \ PriKey (fst (snd (run_asset_ii n s))) \ used s" +by (frule run_owner_ii_nonce [of _ n], drule run_asset_ii_ex [of _ n], auto) + +proposition run_asset_ii_unused: + "s\<^sub>0 \ s \ \C. PriKey C \ used (fst (run_asset_ii n s))" +by (rule prikey_unused, rule rtrancl_trans, simp, rule run_asset_ii_rel) + + +proposition run_owner_iii_ex: + "s\<^sub>0 \ s \ pred_owner_iii n (run_asset_ii n s) (run_owner_iii n s)" +by (drule run_asset_ii_unused, erule exE, subst run_owner_iii_def, rule someI_ex, + auto simp add: split_def) + +proposition run_owner_iii_rel: + "s\<^sub>0 \ s \ s \ fst (run_owner_iii n s)" + (is "_ \ _ \ ?t") +by (rule rtrancl_into_rtrancl, erule run_asset_ii_rel [of _ n], frule run_asset_ii_msg, + drule run_owner_iii_ex, subgoal_tac "(fst (run_asset_ii n s), ?t) \ rel_owner_iii", + simp_all add: rel_def split_def, erule exE, (rule exI)+, auto) + +proposition run_owner_iii_msg: + "s\<^sub>0 \ s \ + case run_owner_iii n s of (s', S, A, B, C, _) \ + {Asset n} \ {Crypt (Auth_ShaKey n) (PriKey S), \Num 2, PubKey B\} \ + {Owner n} \ {\Num 1, PubKey A\, \Num 3, PubKey C\} \ s' \ + (Asset n, PubKey B) \ s'" +by (frule run_asset_ii_msg [of _ n], drule run_owner_iii_ex [of _ n], auto) + +proposition run_owner_iii_nonce: + "s\<^sub>0 \ s \ PriKey (fst (snd (run_owner_iii n s))) \ used s" +by (frule run_asset_ii_nonce [of _ n], drule run_owner_iii_ex [of _ n], auto) + +proposition run_owner_iii_unused: + "s\<^sub>0 \ s \ \D. PriKey D \ used (fst (run_owner_iii n s))" +by (rule prikey_unused, rule rtrancl_trans, simp, rule run_owner_iii_rel) + + +proposition run_asset_iii_ex: + "s\<^sub>0 \ s \ pred_asset_iii n (run_owner_iii n s) (run_asset_iii n s)" +by (drule run_owner_iii_unused, erule exE, subst run_asset_iii_def, rule someI_ex, + auto simp add: split_def) + +proposition run_asset_iii_rel: + "s\<^sub>0 \ s \ s \ fst (run_asset_iii n s)" + (is "_ \ _ \ ?t") +by (rule rtrancl_into_rtrancl, erule run_owner_iii_rel [of _ n], frule run_owner_iii_msg, + drule run_asset_iii_ex, subgoal_tac "(fst (run_owner_iii n s), ?t) \ rel_asset_iii", + simp_all add: rel_def split_def, erule exE, (rule exI)+, auto) + +proposition run_asset_iii_msg: + "s\<^sub>0 \ s \ + case run_asset_iii n s of (s', S, A, B, C, D) \ + {Asset n} \ {Crypt (Auth_ShaKey n) (PriKey S), \Num 2, PubKey B\, + \Num 4, PubKey D\} \ + {Owner n} \ {\Num 1, PubKey A\, \Num 3, PubKey C\} \ s' \ + (Asset n, PubKey B) \ s'" +by (frule run_owner_iii_msg [of _ n], drule run_asset_iii_ex [of _ n], auto) + +proposition run_asset_iii_nonce: + "s\<^sub>0 \ s \ PriKey (fst (snd (run_asset_iii n s))) \ used s" +by (frule run_owner_iii_nonce [of _ n], drule run_asset_iii_ex [of _ n], auto) + + +lemma run_owner_iv_rel_1: + "\s\<^sub>0 \ s; run_asset_iii n s = (s', S, A, B, C, D)\ \ + s \ fst (run_owner_iv n s)" + (is "\_; _\ \ _ \ ?t") +by (rule rtrancl_into_rtrancl, erule run_asset_iii_rel [of _ n], drule run_asset_iii_msg + [of _ n], subgoal_tac "(s', ?t) \ rel_owner_iv", simp_all add: rel_def run_owner_iv_def + Let_def, rule exI [of _ n], rule exI [of _ S], rule exI [of _ A], rule exI [of _ B], + rule exI [of _ C], rule exI [of _ D], rule exI [of _ "Auth_ShaKey n"], auto) + +proposition run_owner_iv_rel: + "s\<^sub>0 \ s \ s \ fst (run_owner_iv n s)" +by (insert run_owner_iv_rel_1, cases "run_asset_iii n s", simp) + +proposition run_owner_iv_msg: + "s\<^sub>0 \ s \ + let (s', S, A, B, C, D) = run_owner_iv n s; + SK = (Some S, {A, B}, {C, D}) in + {Asset n} \ {Crypt (Auth_ShaKey n) (PriKey S), \Num 2, PubKey B\, + \Num 4, PubKey D\} \ + {Owner n} \ {\Num 1, PubKey A\, \Num 3, PubKey C\, SesKey SK, + Crypt (SesK SK) (PubKey D)} \ s' \ + (Asset n, PubKey B) \ s'" +by (drule run_asset_iii_msg [of _ n], simp add: run_owner_iv_def split_def Let_def) + +proposition run_owner_iv_nonce: + "s\<^sub>0 \ s \ PriKey (fst (snd (run_owner_iv n s))) \ used s" +by (drule run_asset_iii_nonce [of _ n], simp add: run_owner_iv_def split_def Let_def) + + +proposition run_asset_iv_rel: + "s\<^sub>0 \ s \ s \ fst (run_asset_iv n s)" + (is "_ \ _ \ ?t") +by (rule rtrancl_into_rtrancl, erule run_owner_iv_rel [of _ n], drule run_owner_iv_msg + [of _ n], subgoal_tac "(fst (run_owner_iv n s), ?t) \ rel_asset_iv", simp_all add: + rel_def run_asset_iv_def split_def Let_def, blast) + +proposition run_asset_iv_msg: + "s\<^sub>0 \ s \ + let (s', S, A, B, C, D) = run_asset_iv n s; SK = (Some S, {A, B}, {C, D}) in + insert (Owner n, SesKey SK) + ({Asset n} \ {SesKey SK, Token n (Auth_PriK n) B C SK}) \ s'" +by (drule run_owner_iv_msg [of _ n], simp add: run_asset_iv_def split_def Let_def) + +proposition run_asset_iv_nonce: + "s\<^sub>0 \ s \ PriKey (fst (snd (run_asset_iv n s))) \ used s" +by (drule run_owner_iv_nonce [of _ n], simp add: run_asset_iv_def split_def Let_def) + + +proposition run_owner_v_rel: + "s\<^sub>0 \ s \ s \ fst (run_owner_v n s)" + (is "_ \ _ \ ?t") +by (rule rtrancl_into_rtrancl, erule run_asset_iv_rel [of _ n], drule run_asset_iv_msg + [of _ n], subgoal_tac "(fst (run_asset_iv n s), ?t) \ rel_owner_v", simp_all add: + rel_def run_owner_v_def split_def Let_def, blast) + +proposition run_owner_v_msg: + "s\<^sub>0 \ s \ + let (s', S, A, B, C, D) = run_owner_v n s; + SK = (Some S, {A, B}, {C, D}) in + {(Asset n, SesKey SK), + (Owner n, Crypt (SesK SK) (Pwd n))} \ s'" +by (drule run_asset_iv_msg [of _ n], simp add: run_owner_v_def split_def Let_def) + +proposition run_owner_v_nonce: + "s\<^sub>0 \ s \ PriKey (fst (snd (run_owner_v n s))) \ used s" +by (drule run_asset_iv_nonce [of _ n], simp add: run_owner_v_def split_def Let_def) + + +proposition run_asset_v_rel: + "s\<^sub>0 \ s \ s \ fst (run_asset_v n s)" + (is "_ \ _ \ ?t") +by (rule rtrancl_into_rtrancl, erule run_owner_v_rel [of _ n], drule run_owner_v_msg + [of _ n], subgoal_tac "(fst (run_owner_v n s), ?t) \ rel_asset_v", simp_all add: + rel_def run_asset_v_def split_def Let_def, blast) + +proposition run_asset_v_msg: + "s\<^sub>0 \ s \ + let (s', S, A, B, C, D) = run_asset_v n s; SK = (Some S, {A, B}, {C, D}) in + {(Owner n, Crypt (SesK SK) (Pwd n)), + (Asset n, Crypt (SesK SK) (Num 0))} \ s'" +by (drule run_owner_v_msg [of _ n], simp add: run_asset_v_def split_def Let_def) + +proposition run_asset_v_nonce: + "s\<^sub>0 \ s \ PriKey (fst (snd (run_asset_v n s))) \ used s" +by (drule run_owner_v_nonce [of _ n], simp add: run_asset_v_def split_def Let_def) + + +lemma runs_unbounded_1: + "\s\<^sub>0 \ s; run_asset_v n s = (s', S, A, B, C, D)\ \ + \s' S SK. (Asset n, Crypt (Auth_ShaKey n) (PriKey S)) \ s \ + {(Owner n, Crypt (SesK SK) (Pwd n)), + (Asset n, Crypt (SesK SK) (Num 0))} \ s' \ + s \ s' \ fst SK = Some S" +by (rule exI [of _ s'], rule exI [of _ S], rule exI [of _ "(Some S, {A, B}, {C, D})"], + rule conjI, rule notI, frule run_asset_v_nonce [of _ n], frule asset_i_used [of _ n S], + simp, frule run_asset_v_rel [of _ n], drule run_asset_v_msg [of _ n], + simp add: Let_def) + +theorem runs_unbounded: + "s\<^sub>0 \ s \ \s' S SK. s \ s' \ fst SK = Some S \ + (Asset n, Crypt (Auth_ShaKey n) (PriKey S)) \ s \ + {(Owner n, Crypt (SesK SK) (Pwd n)), + (Asset n, Crypt (SesK SK) (Num 0))} \ s'" +by (insert runs_unbounded_1, cases "run_asset_v n s", blast) + + +definition pwd_spy_i :: "agent_id \ stage" where +"pwd_spy_i n \ + (insert (Spy, Crypt (Auth_ShaKey n) (Auth_PriKey n)) s\<^sub>0, + Auth_PriK n, 0, 0, 0, 0)" + +definition pwd_owner_ii :: "agent_id \ stage" where +"pwd_owner_ii n \ SOME x. pred_owner_ii n (pwd_spy_i n) x" + +definition pwd_spy_ii :: "agent_id \ stage" where +"pwd_spy_ii n \ + case pwd_owner_ii n of (s, S, A, _) \ + (insert (Spy, \Num 2, PubKey S\) s, S, A, S, 0, 0)" + +definition pwd_owner_iii :: "agent_id \ stage" where +"pwd_owner_iii n \ SOME x. pred_owner_iii n (pwd_spy_ii n) x" + +definition pwd_spy_iii :: "agent_id \ stage" where +"pwd_spy_iii n \ + case pwd_owner_iii n of (s, S, A, B, C, _) \ + (insert (Spy, \Num 4, PubKey S\) s, S, A, B, C, S)" + +definition pwd_owner_iv :: "agent_id \ stage" where +"pwd_owner_iv n \ stage_owner_iv n (pwd_spy_iii n)" + + +definition pwd_spy_sep_map :: "agent_id \ stage" where +"pwd_spy_sep_map n \ + case pwd_owner_iv n of (s, S, A, B, C, D) \ + (insert (Spy, PubKey A) s, S, A, B, C, D)" + +definition pwd_spy_sep_agr :: "agent_id \ stage" where +"pwd_spy_sep_agr n \ + case pwd_spy_sep_map n of (s, S, A, B, C, D) \ + (insert (Spy, PubKey C) s, S, A, B, C, D)" + +definition pwd_spy_sesk :: "agent_id \ stage" where +"pwd_spy_sesk n \ + let (s, S, A, B, C, D) = pwd_spy_sep_agr n; + SK = (Some S, {A, B}, {C, D}) in + (insert (Spy, SesKey SK) s, S, A, B, C, D)" + +definition pwd_spy_mult :: "agent_id \ stage" where +"pwd_spy_mult n \ + case pwd_spy_sesk n of (s, S, A, B, C, D) \ + (insert (Spy, Auth_PriK n \ B) s, S, A, B, C, D)" + +definition pwd_spy_enc_pubk :: "agent_id \ stage" where +"pwd_spy_enc_pubk n \ + let (s, S, A, B, C, D) = pwd_spy_mult n; SK = (Some S, {A, B}, {C, D}) in + (insert (Spy, Crypt (SesK SK) (PubKey C)) s, S, A, B, C, D)" + +definition pwd_spy_enc_mult :: "agent_id \ stage" where +"pwd_spy_enc_mult n \ + let (s, S, A, B, C, D) = pwd_spy_enc_pubk n; + SK = (Some S, {A, B}, {C, D}) in + (insert (Spy, Crypt (SesK SK) (Auth_PriK n \ B)) s, S, A, B, C, D)" + +definition pwd_spy_enc_sign :: "agent_id \ stage" where +"pwd_spy_enc_sign n \ + let (s, S, A, B, C, D) = pwd_spy_enc_mult n; + SK = (Some S, {A, B}, {C, D}) in + (insert (Spy, Crypt (SesK SK) (Sign n (Auth_PriK n))) s, S, A, B, C, D)" + +definition pwd_spy_con :: "agent_id \ stage" where +"pwd_spy_con n \ + let (s, S, A, B, C, D) = pwd_spy_enc_sign n; + SK = (Some S, {A, B}, {C, D}) in + (insert (Spy, \Crypt (SesK SK) (Auth_PriK n \ B), + Crypt (SesK SK) (Sign n (Auth_PriK n))\) s, S, A, B, C, D)" + +definition pwd_spy_iv :: "agent_id \ stage" where +"pwd_spy_iv n \ + let (s, S, A, B, C, D) = pwd_spy_con n; SK = (Some S, {A, B}, {C, D}) in + (insert (Spy, Token n (Auth_PriK n) B C SK) s, S, A, B, C, D)" + + +definition pwd_owner_v :: "agent_id \ stage" where +"pwd_owner_v n \ stage_owner_v n (pwd_spy_iv n)" + +definition pwd_spy_dec :: "agent_id \ stage" where +"pwd_spy_dec n \ + case pwd_owner_v n of (s, S, A, B, C, D) \ + (insert (Spy, Pwd n) s, S, A, B, C, D)" + +definition pwd_spy_id_prik :: "agent_id \ stage" where +"pwd_spy_id_prik n \ + case pwd_spy_dec n of (s, S, A, B, C, D) \ + (insert (Spy, \n, PriKey S\) s, S, A, B, C, D)" + +definition pwd_spy_id_pubk :: "agent_id \ stage" where +"pwd_spy_id_pubk n \ + case pwd_spy_id_prik n of (s, S, A, B, C, D) \ + (insert (Spy, \n, PubKey S\) s, S, A, B, C, D)" + +definition pwd_spy_id_sesk :: "agent_id \ stage" where +"pwd_spy_id_sesk n \ + let (s, S, A, B, C, D) = pwd_spy_id_pubk n; + SK = (Some S, {A, B}, {C, D}) in + (insert (Spy, \n, SesKey SK\) s, S, A, B, C, D)" + +definition pwd_spy_id_pwd :: "agent_id \ stage" where +"pwd_spy_id_pwd n \ + case pwd_spy_id_sesk n of (s, S, A, B, C, D) \ + (insert (Spy, \n, Pwd n\) s, S, A, B, C, D)" + + +proposition key_sets_crypts_subset: + "\U \ key_sets X (crypts (Log -` spied H)); H \ H'\ \ + U \ key_sets X (crypts (Log -` spied H'))" + (is "\_ \ ?A; _\ \ _") +by (rule subsetD [of ?A], rule key_sets_mono, rule crypts_mono, blast) + + +fun pwd_spy_i_state :: "agent_id \ seskey_tuple \ state" where +"pwd_spy_i_state n (S, _) = {Spy} \ ({PriKey S, PubKey S, Key (Auth_ShaKey n), + Auth_PriKey n, Sign n (Auth_PriK n), Crypt (Auth_ShaKey n) (PriKey S), + \n, Key (Auth_ShaKey n)\} \ range Num)" + +proposition pwd_spy_i_rel: + "n \ bad_prikey \ bad_id_shakey \ s\<^sub>0 \ fst (pwd_spy_i n)" + (is "_ \ _ \ ?t") +by (rule r_into_rtrancl, subgoal_tac "(s\<^sub>0, ?t) \ rel_enc", simp_all add: rel_def + pwd_spy_i_def, blast) + +proposition pwd_spy_i_msg: + "n \ bad_prikey \ bad_id_shakey \ + case pwd_spy_i n of (s, S, A, B, C, D) \ + pwd_spy_i_state n (S, A, B, C, D) \ s" +by (simp add: pwd_spy_i_def, blast) + +proposition pwd_spy_i_unused: + "n \ bad_prikey \ bad_id_shakey \ \A. PriKey A \ used (fst (pwd_spy_i n))" +by (drule pwd_spy_i_rel, rule prikey_unused) + + +fun pwd_owner_ii_state :: "agent_id \ seskey_tuple \ state" where +"pwd_owner_ii_state n (S, A, B, C, D) = + pwd_spy_i_state n (S, A, B, C, D) \ {Owner n, Spy} \ {\Num 1, PubKey A\}" + +proposition pwd_owner_ii_ex: + "n \ bad_prikey \ bad_id_shakey \ + pred_owner_ii n (pwd_spy_i n) (pwd_owner_ii n)" +by (drule pwd_spy_i_unused, erule exE, subst pwd_owner_ii_def, rule someI_ex, + auto simp add: split_def) + +proposition pwd_owner_ii_rel: + "n \ bad_prikey \ bad_id_shakey \ s\<^sub>0 \ fst (pwd_owner_ii n)" + (is "_ \ _ \ ?t") +by (rule rtrancl_into_rtrancl, erule pwd_spy_i_rel, frule pwd_spy_i_msg, + drule pwd_owner_ii_ex, subgoal_tac "(fst (pwd_spy_i n), ?t) \ rel_owner_ii", + simp_all add: rel_def split_def, erule exE, rule exI, auto) + +proposition pwd_owner_ii_msg: + "n \ bad_prikey \ bad_id_shakey \ + case pwd_owner_ii n of (s, S, A, B, C, D) \ + pwd_owner_ii_state n (S, A, B, C, D) \ s \ + {Key (Auth_ShaKey n)} \ key_sets (PriKey S) (crypts (Log -` spied s))" +by (frule pwd_spy_i_msg, drule pwd_owner_ii_ex, simp add: split_def, erule exE, + simp add: Image_def, simp only: Collect_disj_eq crypts_union key_sets_union, + simp add: crypts_insert key_sets_insert, blast) + + +fun pwd_spy_ii_state :: "agent_id \ seskey_tuple \ state" where +"pwd_spy_ii_state n (S, A, B, C, D) = + pwd_owner_ii_state n (S, A, B, C, D) \ {Spy} \ {PriKey B, + \Num 2, PubKey B\}" + +proposition pwd_spy_ii_rel: + "n \ bad_prikey \ bad_id_shakey \ s\<^sub>0 \ fst (pwd_spy_ii n)" + (is "_ \ _ \ ?t") +by (rule rtrancl_into_rtrancl, erule pwd_owner_ii_rel, drule pwd_owner_ii_msg, + subgoal_tac "(fst (pwd_owner_ii n), ?t) \ rel_con", simp_all add: rel_def + pwd_spy_ii_def split_def, blast) + +proposition pwd_spy_ii_msg: + "n \ bad_prikey \ bad_id_shakey \ + case pwd_spy_ii n of (s, S, A, B, C, D) \ + pwd_spy_ii_state n (S, A, B, C, D) \ s \ + {Key (Auth_ShaKey n)} \ key_sets (PriKey S) (crypts (Log -` spied s))" +by (drule pwd_owner_ii_msg, simp add: pwd_spy_ii_def split_def, + (erule conjE)+, ((rule conjI | erule key_sets_crypts_subset), blast)+) + +proposition pwd_spy_ii_unused: + "n \ bad_prikey \ bad_id_shakey \ \C. PriKey C \ used (fst (pwd_spy_ii n))" +by (drule pwd_spy_ii_rel, rule prikey_unused) + + +fun pwd_owner_iii_state :: "agent_id \ seskey_tuple \ state" where +"pwd_owner_iii_state n (S, A, B, C, D) = + pwd_spy_ii_state n (S, A, B, C, D) \ {Owner n, Spy} \ {\Num 3, PubKey C\}" + +proposition pwd_owner_iii_ex: + "n \ bad_prikey \ bad_id_shakey \ + pred_owner_iii n (pwd_spy_ii n) (pwd_owner_iii n)" +by (drule pwd_spy_ii_unused, erule exE, subst pwd_owner_iii_def, rule someI_ex, + auto simp add: split_def) + +proposition pwd_owner_iii_rel: + "n \ bad_prikey \ bad_id_shakey \ s\<^sub>0 \ fst (pwd_owner_iii n)" + (is "_ \ _ \ ?t") +by (rule rtrancl_into_rtrancl, erule pwd_spy_ii_rel, frule pwd_spy_ii_msg, + drule pwd_owner_iii_ex, subgoal_tac "(fst (pwd_spy_ii n), ?t) \ rel_owner_iii", + simp_all add: rel_def split_def, rule exI, rule exI, auto) + +proposition pwd_owner_iii_msg: + "n \ bad_prikey \ bad_id_shakey \ + case pwd_owner_iii n of (s, S, A, B, C, D) \ + pwd_owner_iii_state n (S, A, B, C, D) \ s \ + {Key (Auth_ShaKey n)} \ key_sets (PriKey S) (crypts (Log -` spied s))" +by (frule pwd_spy_ii_msg, drule pwd_owner_iii_ex, simp add: split_def, erule exE, + simp, (erule conjE)+, ((rule conjI | erule key_sets_crypts_subset), blast)+) + + +fun pwd_spy_iii_state :: "agent_id \ seskey_tuple \ state" where +"pwd_spy_iii_state n (S, A, B, C, D) = + pwd_owner_iii_state n (S, A, B, C, D) \ {Spy} \ {PriKey D, + \Num 4, PubKey D\}" + +proposition pwd_spy_iii_rel: + "n \ bad_prikey \ bad_id_shakey \ s\<^sub>0 \ fst (pwd_spy_iii n)" + (is "_ \ _ \ ?t") +by (rule rtrancl_into_rtrancl, erule pwd_owner_iii_rel, drule pwd_owner_iii_msg, + subgoal_tac "(fst (pwd_owner_iii n), ?t) \ rel_con", simp_all add: rel_def + pwd_spy_iii_def split_def, blast) + +proposition pwd_spy_iii_msg: + "n \ bad_prikey \ bad_id_shakey \ + case pwd_spy_iii n of (s, S, A, B, C, D) \ + pwd_spy_iii_state n (S, A, B, C, D) \ s \ + {Key (Auth_ShaKey n)} \ key_sets (PriKey S) (crypts (Log -` spied s))" +by (drule pwd_owner_iii_msg, simp add: pwd_spy_iii_def split_def, + (erule conjE)+, ((rule conjI | erule key_sets_crypts_subset), blast)+) + + +fun pwd_owner_iv_state :: "agent_id \ seskey_tuple \ state" where +"pwd_owner_iv_state n (S, A, B, C, D) = (let SK = (Some S, {A, B}, {C, D}) in + insert (Owner n, SesKey SK) (pwd_spy_iii_state n (S, A, B, C, D)))" + +lemma pwd_owner_iv_rel_1: + "\n \ bad_prikey \ bad_id_shakey; pwd_spy_iii n = (s, S, A, B, C, D)\ \ + s\<^sub>0 \ fst (pwd_owner_iv n)" + (is "\_; _\ \ _ \ ?t") +by (rule rtrancl_into_rtrancl, erule pwd_spy_iii_rel, drule pwd_spy_iii_msg, + subgoal_tac "(s, ?t) \ rel_owner_iv", simp_all add: rel_def pwd_owner_iv_def + Let_def, rule exI [of _ n], rule exI [of _ S], rule exI [of _ A], rule exI [of _ B], + rule exI [of _ C], rule exI [of _ D], rule exI [of _ "Auth_ShaKey n"], auto) + +proposition pwd_owner_iv_rel: + "n \ bad_prikey \ bad_id_shakey \ s\<^sub>0 \ fst (pwd_owner_iv n)" +by (insert pwd_owner_iv_rel_1, cases "pwd_spy_iii n", simp) + +proposition pwd_owner_iv_msg: + "n \ bad_prikey \ bad_id_shakey \ + case pwd_owner_iv n of (s, S, A, B, C, D) \ + pwd_owner_iv_state n (S, A, B, C, D) \ s \ + {Key (Auth_ShaKey n)} \ key_sets (PriKey S) (crypts (Log -` spied s))" +by (drule pwd_spy_iii_msg, simp add: pwd_owner_iv_def split_def Let_def, + (erule conjE)+, ((rule conjI | erule key_sets_crypts_subset), blast)+) + + +fun pwd_spy_sep_map_state :: "agent_id \ seskey_tuple \ state" where +"pwd_spy_sep_map_state n (S, A, B, C, D) = + insert (Spy, PubKey A) (pwd_owner_iv_state n (S, A, B, C, D))" + +proposition pwd_spy_sep_map_rel: + "n \ bad_prikey \ bad_id_shakey \ s\<^sub>0 \ fst (pwd_spy_sep_map n)" + (is "_ \ _ \ ?t") +by (rule rtrancl_into_rtrancl, erule pwd_owner_iv_rel, drule pwd_owner_iv_msg, + subgoal_tac "(fst (pwd_owner_iv n), ?t) \ rel_sep", simp_all add: rel_def + pwd_spy_sep_map_def split_def, blast) + +proposition pwd_spy_sep_map_msg: + "n \ bad_prikey \ bad_id_shakey \ + case pwd_spy_sep_map n of (s, S, A, B, C, D) \ + pwd_spy_sep_map_state n (S, A, B, C, D) \ s \ + {Key (Auth_ShaKey n)} \ key_sets (PriKey S) (crypts (Log -` spied s))" +by (drule pwd_owner_iv_msg, simp add: pwd_spy_sep_map_def split_def, + (erule conjE)+, ((rule conjI | erule key_sets_crypts_subset), blast)+) + + +fun pwd_spy_sep_agr_state :: "agent_id \ seskey_tuple \ state" where +"pwd_spy_sep_agr_state n (S, A, B, C, D) = + insert (Spy, PubKey C) (pwd_spy_sep_map_state n (S, A, B, C, D))" + +proposition pwd_spy_sep_agr_rel: + "n \ bad_prikey \ bad_id_shakey \ s\<^sub>0 \ fst (pwd_spy_sep_agr n)" + (is "_ \ _ \ ?t") +by (rule rtrancl_into_rtrancl, erule pwd_spy_sep_map_rel, drule pwd_spy_sep_map_msg, + subgoal_tac "(fst (pwd_spy_sep_map n), ?t) \ rel_sep", simp_all add: rel_def + pwd_spy_sep_agr_def split_def, blast) + +proposition pwd_spy_sep_agr_msg: + "n \ bad_prikey \ bad_id_shakey \ + case pwd_spy_sep_agr n of (s, S, A, B, C, D) \ + pwd_spy_sep_agr_state n (S, A, B, C, D) \ s \ + {Key (Auth_ShaKey n)} \ key_sets (PriKey S) (crypts (Log -` spied s))" +by (drule pwd_spy_sep_map_msg, simp add: pwd_spy_sep_agr_def split_def, + (erule conjE)+, ((rule conjI | erule key_sets_crypts_subset), blast)+) + + +fun pwd_spy_sesk_state :: "agent_id \ seskey_tuple \ state" where +"pwd_spy_sesk_state n (S, A, B, C, D) = (let SK = (Some S, {A, B}, {C, D}) in + insert (Spy, SesKey SK) (pwd_spy_sep_agr_state n (S, A, B, C, D)))" + +proposition pwd_spy_sesk_rel: + "n \ bad_prikey \ bad_id_shakey \ s\<^sub>0 \ fst (pwd_spy_sesk n)" + (is "_ \ _ \ ?t") +by (rule rtrancl_into_rtrancl, erule pwd_spy_sep_agr_rel, drule pwd_spy_sep_agr_msg, + subgoal_tac "(fst (pwd_spy_sep_agr n), ?t) \ rel_sesk", simp_all add: rel_def + pwd_spy_sesk_def split_def Let_def, blast) + +proposition pwd_spy_sesk_msg: + "n \ bad_prikey \ bad_id_shakey \ + case pwd_spy_sesk n of (s, S, A, B, C, D) \ + pwd_spy_sesk_state n (S, A, B, C, D) \ s \ + {Key (Auth_ShaKey n)} \ key_sets (PriKey S) (crypts (Log -` spied s))" +by (drule pwd_spy_sep_agr_msg, simp add: pwd_spy_sesk_def split_def Let_def, + (erule conjE)+, ((rule conjI | erule key_sets_crypts_subset), blast)+) + + +fun pwd_spy_mult_state :: "agent_id \ seskey_tuple \ state" where +"pwd_spy_mult_state n (S, A, B, C, D) = + insert (Spy, Auth_PriK n \ B) (pwd_spy_sesk_state n (S, A, B, C, D))" + +proposition pwd_spy_mult_rel: + "n \ bad_prikey \ bad_id_shakey \ s\<^sub>0 \ fst (pwd_spy_mult n)" + (is "_ \ _ \ ?t") +by (rule rtrancl_into_rtrancl, erule pwd_spy_sesk_rel, drule pwd_spy_sesk_msg, + subgoal_tac "(fst (pwd_spy_sesk n), ?t) \ rel_mult", simp_all add: rel_def + pwd_spy_mult_def split_def, blast) + +proposition pwd_spy_mult_msg: + "n \ bad_prikey \ bad_id_shakey \ + case pwd_spy_mult n of (s, S, A, B, C, D) \ + pwd_spy_mult_state n (S, A, B, C, D) \ s \ + {Key (Auth_ShaKey n)} \ key_sets (PriKey S) (crypts (Log -` spied s))" +by (drule pwd_spy_sesk_msg, simp add: pwd_spy_mult_def split_def, + (erule conjE)+, ((rule conjI | erule key_sets_crypts_subset), blast)+) + + +fun pwd_spy_enc_pubk_state :: "agent_id \ seskey_tuple \ state" where +"pwd_spy_enc_pubk_state n (S, A, B, C, D) = + (let SK = (Some S, {A, B}, {C, D}) in + insert (Spy, Crypt (SesK SK) (PubKey C)) + (pwd_spy_mult_state n (S, A, B, C, D)))" + +proposition pwd_spy_enc_pubk_rel: + "n \ bad_prikey \ bad_id_shakey \ s\<^sub>0 \ fst (pwd_spy_enc_pubk n)" + (is "_ \ _ \ ?t") +by (rule rtrancl_into_rtrancl, erule pwd_spy_mult_rel, drule pwd_spy_mult_msg, + subgoal_tac "(fst (pwd_spy_mult n), ?t) \ rel_enc", simp_all add: rel_def + pwd_spy_enc_pubk_def split_def Let_def, blast) + +proposition pwd_spy_enc_pubk_msg: + "n \ bad_prikey \ bad_id_shakey \ + case pwd_spy_enc_pubk n of (s, S, A, B, C, D) \ + pwd_spy_enc_pubk_state n (S, A, B, C, D) \ s \ + {Key (Auth_ShaKey n)} \ key_sets (PriKey S) (crypts (Log -` spied s))" +by (drule pwd_spy_mult_msg, simp add: pwd_spy_enc_pubk_def split_def Let_def, + (erule conjE)+, ((rule conjI | erule key_sets_crypts_subset), blast)+) + + +fun pwd_spy_enc_mult_state :: "agent_id \ seskey_tuple \ state" where +"pwd_spy_enc_mult_state n (S, A, B, C, D) = + (let SK = (Some S, {A, B}, {C, D}) in + insert (Spy, Crypt (SesK SK) (Auth_PriK n \ B)) + (pwd_spy_enc_pubk_state n (S, A, B, C, D)))" + +proposition pwd_spy_enc_mult_rel: + "n \ bad_prikey \ bad_id_shakey \ s\<^sub>0 \ fst (pwd_spy_enc_mult n)" + (is "_ \ _ \ ?t") +by (rule rtrancl_into_rtrancl, erule pwd_spy_enc_pubk_rel, drule pwd_spy_enc_pubk_msg, + subgoal_tac "(fst (pwd_spy_enc_pubk n), ?t) \ rel_enc", simp_all add: rel_def + pwd_spy_enc_mult_def split_def Let_def, blast) + +proposition pwd_spy_enc_mult_msg: + "n \ bad_prikey \ bad_id_shakey \ + case pwd_spy_enc_mult n of (s, S, A, B, C, D) \ + pwd_spy_enc_mult_state n (S, A, B, C, D) \ s \ + {Key (Auth_ShaKey n)} \ key_sets (PriKey S) (crypts (Log -` spied s))" +by (drule pwd_spy_enc_pubk_msg, simp add: pwd_spy_enc_mult_def split_def Let_def, + (erule conjE)+, ((rule conjI | erule key_sets_crypts_subset), blast)+) + + +fun pwd_spy_enc_sign_state :: "agent_id \ seskey_tuple \ state" where +"pwd_spy_enc_sign_state n (S, A, B, C, D) = + (let SK = (Some S, {A, B}, {C, D}) in + insert (Spy, Crypt (SesK SK) (Sign n (Auth_PriK n))) + (pwd_spy_enc_mult_state n (S, A, B, C, D)))" + +proposition pwd_spy_enc_sign_rel: + "n \ bad_prikey \ bad_id_shakey \ s\<^sub>0 \ fst (pwd_spy_enc_sign n)" + (is "_ \ _ \ ?t") +by (rule rtrancl_into_rtrancl, erule pwd_spy_enc_mult_rel, drule pwd_spy_enc_mult_msg, + subgoal_tac "(fst (pwd_spy_enc_mult n), ?t) \ rel_enc", simp_all add: rel_def + pwd_spy_enc_sign_def split_def Let_def, blast) + +proposition pwd_spy_enc_sign_msg: + "n \ bad_prikey \ bad_id_shakey \ + case pwd_spy_enc_sign n of (s, S, A, B, C, D) \ + pwd_spy_enc_sign_state n (S, A, B, C, D) \ s \ + {Key (Auth_ShaKey n)} \ key_sets (PriKey S) (crypts (Log -` spied s))" +by (drule pwd_spy_enc_mult_msg, simp add: pwd_spy_enc_sign_def split_def Let_def, + (erule conjE)+, ((rule conjI | erule key_sets_crypts_subset), blast)+) + + +fun pwd_spy_con_state :: "agent_id \ seskey_tuple \ state" where +"pwd_spy_con_state n (S, A, B, C, D) = (let SK = (Some S, {A, B}, {C, D}) in + insert (Spy, \Crypt (SesK SK) (Auth_PriK n \ B), + Crypt (SesK SK) (Sign n (Auth_PriK n))\) + (pwd_spy_enc_sign_state n (S, A, B, C, D)))" + +proposition pwd_spy_con_rel: + "n \ bad_prikey \ bad_id_shakey \ s\<^sub>0 \ fst (pwd_spy_con n)" + (is "_ \ _ \ ?t") +by (rule rtrancl_into_rtrancl, erule pwd_spy_enc_sign_rel, drule pwd_spy_enc_sign_msg, + subgoal_tac "(fst (pwd_spy_enc_sign n), ?t) \ rel_con", simp_all add: rel_def + pwd_spy_con_def split_def Let_def, blast) + +proposition pwd_spy_con_msg: + "n \ bad_prikey \ bad_id_shakey \ + case pwd_spy_con n of (s, S, A, B, C, D) \ + pwd_spy_con_state n (S, A, B, C, D) \ s \ + {Key (Auth_ShaKey n)} \ key_sets (PriKey S) (crypts (Log -` spied s))" +by (drule pwd_spy_enc_sign_msg, simp add: pwd_spy_con_def split_def Let_def, + (erule conjE)+, ((rule conjI | erule key_sets_crypts_subset), blast)+) + + +fun pwd_spy_iv_state :: "agent_id \ seskey_tuple \ state" where +"pwd_spy_iv_state n (S, A, B, C, D) = (let SK = (Some S, {A, B}, {C, D}) in + insert (Spy, Token n (Auth_PriK n) B C SK) + (pwd_spy_con_state n (S, A, B, C, D)))" + +proposition pwd_spy_iv_rel: + "n \ bad_prikey \ bad_id_shakey \ s\<^sub>0 \ fst (pwd_spy_iv n)" + (is "_ \ _ \ ?t") +by (rule rtrancl_into_rtrancl, erule pwd_spy_con_rel, drule pwd_spy_con_msg, + subgoal_tac "(fst (pwd_spy_con n), ?t) \ rel_con", simp_all add: rel_def + pwd_spy_iv_def split_def Let_def, blast) + +proposition pwd_spy_iv_msg: + "n \ bad_prikey \ bad_id_shakey \ + case pwd_spy_iv n of (s, S, A, B, C, D) \ + pwd_spy_iv_state n (S, A, B, C, D) \ s \ + {Key (Auth_ShaKey n)} \ key_sets (PriKey S) (crypts (Log -` spied s))" +by (drule pwd_spy_con_msg, simp add: pwd_spy_iv_def split_def Let_def, + (erule conjE)+, ((rule conjI | erule key_sets_crypts_subset), blast)+) + + +fun pwd_owner_v_state :: "agent_id \ seskey_tuple \ state" where +"pwd_owner_v_state n (S, A, B, C, D) = (let SK = (Some S, {A, B}, {C, D}) in + insert (Spy, Crypt (SesK SK) (Pwd n)) (pwd_spy_iv_state n (S, A, B, C, D)))" + +proposition pwd_owner_v_rel: + "n \ bad_prikey \ bad_id_shakey \ s\<^sub>0 \ fst (pwd_owner_v n)" + (is "_ \ _ \ ?t") +by (rule rtrancl_into_rtrancl, erule pwd_spy_iv_rel, drule pwd_spy_iv_msg, + subgoal_tac "(fst (pwd_spy_iv n), ?t) \ rel_owner_v", simp_all add: rel_def + pwd_owner_v_def split_def Let_def, (rule exI)+, blast) + +proposition pwd_owner_v_msg: + "n \ bad_prikey \ bad_id_shakey \ + let (s, S, A, B, C, D) = pwd_owner_v n; SK = (Some S, {A, B}, {C, D}) in + pwd_owner_v_state n (S, A, B, C, D) \ s \ + {Key (Auth_ShaKey n)} \ key_sets (PriKey S) (crypts (Log -` spied s)) \ + {SesKey SK} \ key_sets (Pwd n) (crypts (Log -` spied s))" +by (drule pwd_spy_iv_msg, simp add: pwd_owner_v_def split_def Let_def, (erule conjE)+, + (rule conjI, (erule key_sets_crypts_subset)?, blast)+, simp add: Image_def, simp + only: Collect_disj_eq crypts_union key_sets_union, simp add: crypts_insert + key_sets_insert) + + +abbreviation pwd_spy_dec_state :: "agent_id \ seskey_tuple \ state" where +"pwd_spy_dec_state n x \ insert (Spy, Pwd n) (pwd_owner_v_state n x)" + +proposition pwd_spy_dec_rel: + "n \ bad_prikey \ bad_id_shakey \ s\<^sub>0 \ fst (pwd_spy_dec n)" + (is "_ \ _ \ ?t") +by (rule rtrancl_into_rtrancl, erule pwd_owner_v_rel, drule pwd_owner_v_msg, + subgoal_tac "(fst (pwd_owner_v n), ?t) \ rel_dec", simp_all add: rel_def + pwd_spy_dec_def split_def Let_def, (rule exI)+, auto) + +proposition pwd_spy_dec_msg: + "n \ bad_prikey \ bad_id_shakey \ + let (s, S, A, B, C, D) = pwd_spy_dec n; SK = (Some S, {A, B}, {C, D}) in + pwd_spy_dec_state n (S, A, B, C, D) \ s \ + {Key (Auth_ShaKey n)} \ key_sets (PriKey S) (crypts (Log -` spied s)) \ + {SesKey SK} \ key_sets (Pwd n) (crypts (Log -` spied s))" +by (drule pwd_owner_v_msg, simp add: pwd_spy_dec_def split_def Let_def, + (erule conjE)+, ((rule conjI)?, (erule key_sets_crypts_subset)?, blast)+) + + +fun pwd_spy_id_prik_state :: "agent_id \ seskey_tuple \ state" where +"pwd_spy_id_prik_state n (S, A, B, C, D) = + insert (Spy, \n, PriKey S\) (pwd_spy_dec_state n (S, A, B, C, D))" + +proposition pwd_spy_id_prik_rel: + "n \ bad_prikey \ bad_id_shakey \ s\<^sub>0 \ fst (pwd_spy_id_prik n)" + (is "_ \ _ \ ?t") +by (rule rtrancl_into_rtrancl, erule pwd_spy_dec_rel, drule pwd_spy_dec_msg, + subgoal_tac "(fst (pwd_spy_dec n), ?t) \ rel_id_crypt", simp_all add: rel_def + pwd_spy_id_prik_def split_def Let_def, (rule exI)+, blast) + +proposition pwd_spy_id_prik_msg: + "n \ bad_prikey \ bad_id_shakey \ + let (s, S, A, B, C, D) = pwd_spy_id_prik n; + SK = (Some S, {A, B}, {C, D}) in + pwd_spy_id_prik_state n (S, A, B, C, D) \ s \ + {SesKey SK} \ key_sets (Pwd n) (crypts (Log -` spied s))" +by (drule pwd_spy_dec_msg, simp add: pwd_spy_id_prik_def split_def Let_def, + (erule conjE)+, ((rule conjI | erule key_sets_crypts_subset), blast)+) + + +fun pwd_spy_id_pubk_state :: "agent_id \ seskey_tuple \ state" where +"pwd_spy_id_pubk_state n (S, A, B, C, D) = + insert (Spy, \n, PubKey S\) (pwd_spy_id_prik_state n (S, A, B, C, D))" + +proposition pwd_spy_id_pubk_rel: + "n \ bad_prikey \ bad_id_shakey \ s\<^sub>0 \ fst (pwd_spy_id_pubk n)" + (is "_ \ _ \ ?t") +by (rule rtrancl_into_rtrancl, erule pwd_spy_id_prik_rel, drule pwd_spy_id_prik_msg, + subgoal_tac "(fst (pwd_spy_id_prik n), ?t) \ rel_id_invk", simp_all add: rel_def + pwd_spy_id_pubk_def split_def Let_def, (rule exI)+, auto) + +proposition pwd_spy_id_pubk_msg: + "n \ bad_prikey \ bad_id_shakey \ + let (s, S, A, B, C, D) = pwd_spy_id_pubk n; + SK = (Some S, {A, B}, {C, D}) in + pwd_spy_id_pubk_state n (S, A, B, C, D) \ s \ + {SesKey SK} \ key_sets (Pwd n) (crypts (Log -` spied s))" +by (drule pwd_spy_id_prik_msg, simp add: pwd_spy_id_pubk_def split_def Let_def, + (erule conjE)+, ((rule conjI | erule key_sets_crypts_subset), blast)+) + + +fun pwd_spy_id_sesk_state :: "agent_id \ seskey_tuple \ state" where +"pwd_spy_id_sesk_state n (S, A, B, C, D) = + (let SK = (Some S, {A, B}, {C, D}) in + insert (Spy, \n, SesKey SK\) (pwd_spy_id_pubk_state n (S, A, B, C, D)))" + +proposition pwd_spy_id_sesk_rel: + "n \ bad_prikey \ bad_id_shakey \ s\<^sub>0 \ fst (pwd_spy_id_sesk n)" + (is "_ \ _ \ ?t") +by (rule rtrancl_into_rtrancl, erule pwd_spy_id_pubk_rel, drule pwd_spy_id_pubk_msg, + subgoal_tac "(fst (pwd_spy_id_pubk n), ?t) \ rel_id_sesk", simp_all add: rel_def + pwd_spy_id_sesk_def split_def Let_def, rule exI, rule exI, rule exI + [of _ "Some (fst (snd (pwd_spy_id_pubk n)))"], auto) + +proposition pwd_spy_id_sesk_msg: + "n \ bad_prikey \ bad_id_shakey \ + let (s, S, A, B, C, D) = pwd_spy_id_sesk n; + SK = (Some S, {A, B}, {C, D}) in + pwd_spy_id_sesk_state n (S, A, B, C, D) \ s \ + {SesKey SK} \ key_sets (Pwd n) (crypts (Log -` spied s))" +by (drule pwd_spy_id_pubk_msg, simp add: pwd_spy_id_sesk_def split_def Let_def, + (erule conjE)+, ((rule conjI | erule key_sets_crypts_subset), blast)+) + + +abbreviation pwd_spy_id_pwd_state :: "agent_id \ seskey_tuple \ state" where +"pwd_spy_id_pwd_state n x \ insert (Spy, \n, Pwd n\) (pwd_spy_id_sesk_state n x)" + +proposition pwd_spy_id_pwd_rel: + "n \ bad_prikey \ bad_id_shakey \ s\<^sub>0 \ fst (pwd_spy_id_pwd n)" + (is "_ \ _ \ ?t") +by (rule rtrancl_into_rtrancl, erule pwd_spy_id_sesk_rel, drule pwd_spy_id_sesk_msg, + subgoal_tac "(fst (pwd_spy_id_sesk n), ?t) \ rel_id_crypt", simp_all add: rel_def + pwd_spy_id_pwd_def split_def Let_def, (rule exI)+, blast) + +proposition pwd_spy_id_pwd_msg: + "n \ bad_prikey \ bad_id_shakey \ + case pwd_spy_id_pwd n of (s, S, A, B, C, D) \ + pwd_spy_id_pwd_state n (S, A, B, C, D) \ s" +by (drule pwd_spy_id_sesk_msg, simp add: pwd_spy_id_pwd_def split_def Let_def, + blast) + + +theorem pwd_compromised: + "n \ bad_prikey \ bad_id_shakey \ \s. s\<^sub>0 \ s \ {Pwd n, \n, Pwd n\} \ spied s" +by (rule exI [of _ "fst (pwd_spy_id_pwd n)"], rule conjI, erule pwd_spy_id_pwd_rel, + drule pwd_spy_id_pwd_msg, simp add: split_def) + + +end diff --git a/thys/Relational_Method/ROOT b/thys/Relational_Method/ROOT new file mode 100644 --- /dev/null +++ b/thys/Relational_Method/ROOT @@ -0,0 +1,13 @@ +chapter AFP + +session Relational_Method (AFP) = "HOL" + + description \The Relational Method with Message Anonymity for the Verification of Cryptographic Protocols\ + options [timeout = 300] + theories + Definitions + Authentication + Anonymity + Possibility + document_files + "root.bib" + "root.tex" diff --git a/thys/Relational_Method/document/root.bib b/thys/Relational_Method/document/root.bib new file mode 100644 --- /dev/null +++ b/thys/Relational_Method/document/root.bib @@ -0,0 +1,59 @@ +@article { + Paulson98, + author = {Lawrence C. Paulson}, + title = {The Inductive Approach to Verifying Cryptographic Protocols}, + journal = {Journal of Computer Security}, + month = dec, + year = 1998 +} + +@article { + Noce17, + author = {Pasquale Noce}, + title = {Verification of a Diffie-Hellman Password-based Authentication Protocol by Extending the Inductive Method}, + journal = {Archive of Formal Proofs}, + month = jan, + year = 2017, + note = {\url{http://isa-afp.org/entries/Password_Authentication_Protocol.html}, Formal proof development}, + ISSN = {2150-914x} +} + +@manual { + ICAO15, + title = {Doc 9303 -- Machine Readable Travel Documents -- Part 11: Security Mechanisms for MRTDs}, + organization = {International Civil Aviation Organization (ICAO)}, + edition = {7th}, + year = 2015 +} + +@manual{ + Paulson20, + author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel}, + title = {Isabelle/HOL -- A Proof Assistant for Higher-Order Logic}, + month = apr, + year = 2020, + note = {\url{https://isabelle.in.tum.de/website-Isabelle2020/dist/Isabelle2020/doc/tutorial.pdf}} +} + +@manual{ + Nipkow20, + author = {Tobias Nipkow}, + title = {Programming and Proving in Isabelle/HOL}, + month = apr, + year = 2020, + note = {\url{https://isabelle.in.tum.de/website-Isabelle2020/dist/Isabelle2020/doc/prog-prove.pdf}} +} + +@manual{ + Krauss20, + author = {Alexander Krauss}, + title = {Defining Recursive Functions in Isabelle/HOL}, + note = {\url{https://isabelle.in.tum.de/website-Isabelle2020/dist/Isabelle2020/doc/functions.pdf}} +} + +@manual{ + Nipkow11, + author = {Tobias Nipkow}, + title = {A Tutorial Introduction to Structured Isar Proofs}, + note = {\url{https://isabelle.in.tum.de/website-Isabelle2011/dist/Isabelle2011/doc/isar-overview.pdf}} +} diff --git a/thys/Relational_Method/document/root.tex b/thys/Relational_Method/document/root.tex new file mode 100644 --- /dev/null +++ b/thys/Relational_Method/document/root.tex @@ -0,0 +1,68 @@ +\documentclass[11pt,a4paper,fleqn]{article} +\usepackage{isabelle,isabellesym} +\renewcommand{\isastyletxt}{\isastyletext} + +% further packages required for unusual symbols (see also +% isabellesym.sty), use only when needed + +%\usepackage{amssymb} + %for \, \, \, \, \, \, + %\, \, \, \, \, + %\, \, \ + +%\usepackage{eurosym} + %for \ + +%\usepackage[only,bigsqcap]{stmaryrd} + %for \ + +%\usepackage{eufrak} + %for \ ... \, \ ... \ (also included in amssymb) + +%\usepackage{textcomp} + %for \, \, \, \, \, + %\ + +% this should be the last package used +\usepackage{pdfsetup} + +% urls in roman style, theory text in math-similar italics +\urlstyle{rm} +\isabellestyle{it} + +% for uniform font size +%\renewcommand{\isastyle}{\isastyleminor} + + +\begin{document} + +\title{The Relational Method with Message Anonymity\\for the Verification of Cryptographic Protocols} +\author{Pasquale Noce\\Software Engineer at HID Global, Italy\\pasquale dot noce dot lavoro at gmail dot com\\pasquale dot noce at hidglobal dot com} +\maketitle + +\begin{abstract} +This paper introduces a new method for the formal verification of cryptographic protocols, the +relational method, derived from Paulson's inductive method by means of some enhancements aimed at +streamlining formal definitions and proofs, specially for protocols using public key cryptography. +Moreover, this paper proposes a method to formalize a further security property, message anonymity, +in addition to message confidentiality and authenticity. + +The relational method, including message anonymity, is then applied to the verification of a sample +authentication protocol, comprising Password Authenticated Connection Establishment (PACE) with Chip +Authentication Mapping followed by the explicit verification of an additional password over the PACE +secure channel. +\end{abstract} + +\tableofcontents + +% sane default for proof documents +\parindent 0pt\parskip 0.5ex + +% generated text of all theories +\input{session} + +% bibliography +\bibliographystyle{abbrv} +\bibliography{root} + +\end{document}