Loading theory "Key_Agreement_Strong_Adversaries.Infra"
Loading theory "Key_Agreement_Strong_Adversaries.Messages"
### theory "Key_Agreement_Strong_Adversaries.Infra"
### 0.126s elapsed time, 0.348s cpu time, 0.000s GC time
Loading theory "Key_Agreement_Strong_Adversaries.Refinement"
Proofs for inductive predicate(s) "reachp"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
Proofs for inductive predicate(s) "behp"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
Found termination order: "{}"
Found termination order: "{}"
Proofs for inductive predicate(s) "seq_liftp"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
### theory "Key_Agreement_Strong_Adversaries.Refinement"
### 1.864s elapsed time, 3.680s cpu time, 0.336s GC time
Found termination order: "{}"
Proofs for inductive predicate(s) "eq"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
### Rule already declared as introduction (intro)
### \<lbrakk>eq ?a ?b; eq ?b ?c\<rbrakk> \<Longrightarrow> eq ?a ?c
### Rule already declared as introduction (intro)
### \<lbrakk>eq ?a ?b; eq ?b ?c\<rbrakk> \<Longrightarrow> eq ?a ?c
### Rule already declared as introduction (intro)
### \<lbrakk>eq ?a ?b; eq ?b ?c\<rbrakk> \<Longrightarrow> eq ?a ?c
### Rule already declared as introduction (intro)
### \<lbrakk>eq ?a ?b; eq ?b ?c\<rbrakk> \<Longrightarrow> eq ?a ?c
### Rule already declared as introduction (intro)
### \<lbrakk>eq ?a ?b; eq ?b ?c\<rbrakk> \<Longrightarrow> eq ?a ?c
### Rule already declared as introduction (intro)
### \<lbrakk>eq ?a ?b; eq ?b ?c\<rbrakk> \<Longrightarrow> eq ?a ?c
### theory "Key_Agreement_Strong_Adversaries.Messages"
### 5.829s elapsed time, 11.672s cpu time, 0.796s GC time
Loading theory "Key_Agreement_Strong_Adversaries.AuthenticationN"
Loading theory "Key_Agreement_Strong_Adversaries.Message_derivation"
Proofs for inductive predicate(s) "synthp"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
Proofs for inductive predicate(s) "analzp"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
Found termination order: "{}"
Proofs for inductive predicate(s) "partsp"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
### theory "Key_Agreement_Strong_Adversaries.AuthenticationN"
### 1.172s elapsed time, 2.356s cpu time, 0.000s GC time
Loading theory "Key_Agreement_Strong_Adversaries.AuthenticationI"
### theory "Key_Agreement_Strong_Adversaries.Message_derivation"
### 1.145s elapsed time, 2.304s cpu time, 0.000s GC time
Loading theory "Key_Agreement_Strong_Adversaries.Channels"
### theory "Key_Agreement_Strong_Adversaries.AuthenticationI"
### 0.137s elapsed time, 0.276s cpu time, 0.000s GC time
Loading theory "Key_Agreement_Strong_Adversaries.IK"
### theory "Key_Agreement_Strong_Adversaries.IK"
### 0.236s elapsed time, 0.472s cpu time, 0.000s GC time
Loading theory "Key_Agreement_Strong_Adversaries.Secrecy"
Proofs for inductive predicate(s) "extrp"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
Proofs for inductive predicate(s) "fakep"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
### theory "Key_Agreement_Strong_Adversaries.Channels"
### 1.225s elapsed time, 2.408s cpu time, 0.596s GC time
Loading theory "Key_Agreement_Strong_Adversaries.Payloads"
Proofs for inductive predicate(s) "cpayloadp"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
### theory "Key_Agreement_Strong_Adversaries.Secrecy"
### 1.001s elapsed time, 1.956s cpu time, 0.596s GC time
Loading theory "Key_Agreement_Strong_Adversaries.Runs"
### theory "Key_Agreement_Strong_Adversaries.Payloads"
### 0.798s elapsed time, 1.604s cpu time, 0.000s GC time
Loading theory "Key_Agreement_Strong_Adversaries.Implem"
locale basic_implem
  fixes implem :: "chan \<Rightarrow> msg"
locale semivalid_implem
  fixes implem :: "chan \<Rightarrow> msg"
  assumes "semivalid_implem implem"
locale valid_implem
  fixes implem :: "chan \<Rightarrow> msg"
  assumes "valid_implem implem"
### theory "Key_Agreement_Strong_Adversaries.Implem"
### 0.446s elapsed time, 0.892s cpu time, 0.000s GC time
Loading theory "Key_Agreement_Strong_Adversaries.Implem_asymmetric"
Found termination order: "{}"
Found termination order: "{}"
Found termination order: "{}"
### theory "Key_Agreement_Strong_Adversaries.Runs"
### 1.341s elapsed time, 2.696s cpu time, 0.000s GC time
Loading theory "Key_Agreement_Strong_Adversaries.Implem_lemmas"
locale semivalid_implem
  fixes implem :: "chan \<Rightarrow> msg"
  assumes "semivalid_implem implem"
### theory "Key_Agreement_Strong_Adversaries.Implem_asymmetric"
### 0.429s elapsed time, 0.860s cpu time, 0.000s GC time
Loading theory "Key_Agreement_Strong_Adversaries.Implem_symmetric"
### theory "Key_Agreement_Strong_Adversaries.Implem_lemmas"
### 0.312s elapsed time, 0.624s cpu time, 0.000s GC time
Loading theory "Key_Agreement_Strong_Adversaries.dhlvl1"
Found termination order: "{}"
### theory "Key_Agreement_Strong_Adversaries.Implem_symmetric"
### 0.460s elapsed time, 0.924s cpu time, 0.000s GC time
Loading theory "Key_Agreement_Strong_Adversaries.pfslvl1"
Found termination order: "{}"
specification
  guessed_frame_dom_spec: dom (guessed_frame ?R) = domain (role (guessed_runs ?R))
  guessed_frame_payload_spec: guessed_frame ?R ?x = Some ?y \<Longrightarrow> ?y \<in> payload
  guessed_frame_Init_xnx: role (guessed_runs ?R) = Init \<Longrightarrow>
guessed_frame ?R xnx = Some (NonceF (?R $ nx))
  guessed_frame_Init_xgnx: role (guessed_runs ?R) = Init \<Longrightarrow>
guessed_frame ?R xgnx = Some (Exp Gen (NonceF (?R $ nx)))
  guessed_frame_Resp_xny: role (guessed_runs ?R) = Resp \<Longrightarrow>
guessed_frame ?R xny = Some (NonceF (?R $ ny))
  guessed_frame_Resp_xgny: role (guessed_runs ?R) = Resp \<Longrightarrow>
guessed_frame ?R xgny = Some (Exp Gen (NonceF (?R $ ny)))
  guessed_frame_xEnd: guessed_frame ?R xEnd = Some End
Found termination order: "{}"
specification
  guessed_frame_dom_spec: dom (guessed_frame ?R) = domain (role (guessed_runs ?R))
  guessed_frame_payload_spec: guessed_frame ?R ?x = Some ?y \<Longrightarrow> ?y \<in> payload
  guessed_frame_Init_xpkE: role (guessed_runs ?R) = Init \<Longrightarrow>
guessed_frame ?R xpkE = Some (epubKF (?R $ kE))
  guessed_frame_Init_xskE: role (guessed_runs ?R) = Init \<Longrightarrow>
guessed_frame ?R xskE = Some (epriKF (?R $ kE))
  guessed_frame_Resp_xsk: role (guessed_runs ?R) = Resp \<Longrightarrow>
guessed_frame ?R xsk = Some (NonceF (?R $ sk))
### theory "Key_Agreement_Strong_Adversaries.dhlvl1"
### 1.164s elapsed time, 2.336s cpu time, 0.000s GC time
### theory "Key_Agreement_Strong_Adversaries.pfslvl1"
### 1.341s elapsed time, 2.648s cpu time, 0.588s GC time
### Rule already declared as introduction (intro)
### \<lbrakk>eq ?a ?b; eq ?b ?c\<rbrakk> \<Longrightarrow> eq ?a ?c
### Ignoring duplicate elimination (elim)
### \<lbrakk>?X \<in> synth (analz ?H); ?c \<in> parts (insert ?X ?H);
###  ?c \<in> synth (analz ?H) \<union> parts ?H \<Longrightarrow>
###  PROP ?W\<rbrakk>
### \<Longrightarrow> PROP ?W
### Rule already declared as introduction (intro)
### {?pre} ?Ra ?x, ?Rc {> ?post} \<Longrightarrow>
### {?pre} \<Union>x. ?Ra x, ?Rc {> ?post}
### Rule already declared as introduction (intro)
### \<lbrakk>?M \<in> ?IK;
###  ?c = insec \<or>
###  ?c = confid \<or> ?A \<in> ?bad \<or> ?B \<in> ?bad\<rbrakk>
### \<Longrightarrow> Chan ?c ?A ?B ?M \<in> fake ?bad ?IK ?chan
### Rule already declared as elimination (elim)
### \<lbrakk>Enc ?X ?Y \<in> payload;
###  \<lbrakk>?X \<in> payload; ?Y \<in> payload\<rbrakk>
###  \<Longrightarrow> ?P\<rbrakk>
### \<Longrightarrow> ?P
### Ignoring duplicate elimination (elim)
### \<lbrakk>?X \<in> local.abs ?H;
###  \<And>x A B M.
###     \<lbrakk>?X = Chan x A B M; M \<in> payload; implem ?X \<in> ?H\<rbrakk>
###     \<Longrightarrow> ?P\<rbrakk>
### \<Longrightarrow> ?P
### Rule already declared as elimination (elim)
### \<lbrakk>?X \<in> parts ?S; ?S \<subseteq> payload;
###  ?X \<in> payload \<Longrightarrow> PROP ?W\<rbrakk>
### \<Longrightarrow> PROP ?W
### Rule already declared as elimination (elim)
### \<lbrakk>Hash ?X \<in> payload;
###  ?X \<in> payload \<Longrightarrow> ?P\<rbrakk>
### \<Longrightarrow> ?P
\<lbrakk>?x \<in> analz ?H; \<And>X. X \<in> ?H \<Longrightarrow> ?P X;
 \<And>X Y.
    \<lbrakk>\<langle>X, Y\<rangle> \<in> analz ?H;
     ?P \<langle>X, Y\<rangle>\<rbrakk>
    \<Longrightarrow> ?P X;
 \<And>X Y.
    \<lbrakk>\<langle>X, Y\<rangle> \<in> analz ?H;
     ?P \<langle>X, Y\<rangle>\<rbrakk>
    \<Longrightarrow> ?P Y;
 \<And>X Y.
    \<lbrakk>Enc X Y \<in> analz ?H; ?P (Enc X Y);
     Y \<in> synth (analz ?H \<inter> Collect ?P)\<rbrakk>
    \<Longrightarrow> ?P X;
 \<And>X Y.
    \<lbrakk>Aenc X (pubK Y) \<in> analz ?H; ?P (Aenc X (pubK Y));
     priK Y \<in> analz ?H; ?P (priK Y)\<rbrakk>
    \<Longrightarrow> ?P X;
 \<And>X Y.
    \<lbrakk>Aenc X (epubK Y) \<in> analz ?H; ?P (Aenc X (epubK Y));
     epriK Y \<in> synth (analz ?H \<inter> Collect ?P)\<rbrakk>
    \<Longrightarrow> ?P X;
 \<And>X Y.
    \<lbrakk>Sign X (priK Y) \<in> analz ?H; ?P (Sign X (priK Y));
     pubK Y \<in> analz ?H; ?P (pubK Y)\<rbrakk>
    \<Longrightarrow> ?P X\<rbrakk>
\<Longrightarrow> ?P ?x
isabelle document -d /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Key_Agreement_Strong_Adversaries/document -o pdf -n document
isabelle document -d /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Key_Agreement_Strong_Adversaries/outline -o pdf -n outline -t /proof,/ML
*** Failed to load theory "Key_Agreement_Strong_Adversaries.dhlvl2" (unresolved "Key_Agreement_Strong_Adversaries.dhlvl1")
*** Failed to load theory "Key_Agreement_Strong_Adversaries.dhlvl3" (unresolved "Key_Agreement_Strong_Adversaries.dhlvl2")
*** Failed to load theory "Key_Agreement_Strong_Adversaries.dhlvl3_asymmetric" (unresolved "Key_Agreement_Strong_Adversaries.dhlvl3")
*** Failed to load theory "Key_Agreement_Strong_Adversaries.dhlvl3_symmetric" (unresolved "Key_Agreement_Strong_Adversaries.dhlvl3")
*** Failed to load theory "Key_Agreement_Strong_Adversaries.sklvl1" (unresolved "Key_Agreement_Strong_Adversaries.dhlvl1")
*** Failed to load theory "Key_Agreement_Strong_Adversaries.sklvl2" (unresolved "Key_Agreement_Strong_Adversaries.sklvl1")
*** Failed to load theory "Key_Agreement_Strong_Adversaries.sklvl3" (unresolved "Key_Agreement_Strong_Adversaries.sklvl2")
*** Failed to load theory "Key_Agreement_Strong_Adversaries.sklvl3_asymmetric" (unresolved "Key_Agreement_Strong_Adversaries.sklvl3")
*** Failed to load theory "Key_Agreement_Strong_Adversaries.sklvl3_symmetric" (unresolved "Key_Agreement_Strong_Adversaries.sklvl3")
*** Failed to load theory "Key_Agreement_Strong_Adversaries.pfslvl2" (unresolved "Key_Agreement_Strong_Adversaries.pfslvl1")
*** Failed to load theory "Key_Agreement_Strong_Adversaries.pfslvl3" (unresolved "Key_Agreement_Strong_Adversaries.pfslvl2")
*** Failed to load theory "Key_Agreement_Strong_Adversaries.pfslvl3_asymmetric" (unresolved "Key_Agreement_Strong_Adversaries.pfslvl3")
*** Failed to load theory "Key_Agreement_Strong_Adversaries.pfslvl3_symmetric" (unresolved "Key_Agreement_Strong_Adversaries.pfslvl3")
*** Type unification failed: Clash of types "_ set" and "_ \<Rightarrow> _"
*** 
*** Type error in application: incompatible operand type
*** 
*** Operator:  l1_state_ext ::
***   (fid_t \<Rightarrow> Runs.var set option)
***   \<Rightarrow> (signal \<Rightarrow> nat)
***                 \<Rightarrow> ??'a
***                               \<Rightarrow> \<lparr>progress ::
***                 fid_t \<Rightarrow> Runs.var set option,
***          signals :: signal \<Rightarrow> nat, \<dots> :: ??'a\<rparr>
*** Operand:   {} :: ??'b set
*** 
*** At command "definition" (line 235 of "~~/afp/thys/Key_Agreement_Strong_Adversaries/pfslvl1.thy")
*** Type unification failed: Clash of types "_ set" and "_ \<Rightarrow> _"
*** 
*** Type error in application: incompatible operand type
*** 
*** Operator:  l1_state_ext ::
***   (fid_t \<Rightarrow> Runs.var set option)
***   \<Rightarrow> (signal \<Rightarrow> nat)
***                 \<Rightarrow> (signal \<Rightarrow> nat)
***                               \<Rightarrow> ??'a
***       \<Rightarrow> \<lparr>progress ::
***                               fid_t \<Rightarrow> Runs.var set option,
***                        signalsInit :: signal \<Rightarrow> nat,
***                        signalsResp :: signal \<Rightarrow> nat,
***                        \<dots> :: ??'a\<rparr>
*** Operand:   {} :: ??'b set
*** 
*** At command "definition" (line 287 of "~~/afp/thys/Key_Agreement_Strong_Adversaries/dhlvl1.thy")