Commit e3a47c51 authored by Adrien Koutsos's avatar Adrien Koutsos

presentation gdt secsi

parent a876fa3e
Pipeline #2010 passed with stage
in 1 minute and 32 seconds
......@@ -6,4 +6,9 @@ todo
output.tex
*.aux
*.log
*.pdf
\ No newline at end of file
*.pdf
*.snm
*.nav
*.toc
*.synctex.gz
*.out
\ No newline at end of file
......@@ -2,13 +2,15 @@ OCB_FLAGS = -use-ocamlfind -use-menhir -I src -pkgs ANSITerminal -pkgs fmt -pk
OCB = ocamlbuild $(OCB_FLAGS)
all: byte
clean:
$(OCB) -clean
native: sanity
$(OCB) main.native
all byte: sanity
byte: sanity
$(OCB) main.byte
profile: sanity
......
find . -regex ".*\.\(ml\|tex\|mli\|mly\|mll\|el\)" | grep -v _build | xargs cat | wc -l
\newcommand{\pvec}[1]{\vec{#1}\mkern2mu\vphantom{#1}}
\newcommand{\todo}[1]{\textcolor{red}{(\textbf{A:} #1)}}
% Color
\definecolor{goodgreen}{rgb}{0.20,0.43,0.09}
\newcommand{\blue}[1]{{\color{blue} #1}}
\newcommand{\green}[1]{{\color{goodgreen} #1}}
\newcommand{\red}[1]{{\color{red} #1}}
\newcommand{\purple}[1]{{\color{purple} #1}}
% RFID Protocol Names
\newcommand{\kcl}{\ensuremath{\text{KCL}}\xspace}
\newcommand{\kclp}{\ensuremath{\text{KCL}^+}\xspace}
\newcommand{\lak}{\ensuremath{\text{LAK}}\xspace}
\newcommand{\rfid}{RFID\xspace}
\newcommand{\lakp}{\ensuremath{\text{LAK}^+}\xspace}
\newcommand{\agent}[1]{\textcolor{goodgreen}{\textsf{#1}}}
% Term Functions
\newcommand{\nonce}[1]{\textcolor{red}{\textsf{n}_{\textsf{#1}}}}
\newcommand{\pnonce}[1]{\textcolor{red}{\textsf{n'}_{\textsf{#1}}}}
\newcommand{\noncep}[1]{\textcolor{red}{\textsf{n}'_{\textsf{#1}}}}
\newcommand{\rsample}{\overset{\$}{\leftarrow}}
\newcommand{\hash}{\textsf{H}}
\newcommand{\ow}{\textsf{h}}
\newcommand{\key}[1]{\textcolor{blue}{\textsf{k}_{\textsf{#1}}}}
\newcommand{\false}{\textcolor{magenta}{\textsf{false}}}
\newcommand{\eq}[2]{\textsf{EQ}(#1;#2)}
\newcommand{\beq}[2]{\textsf{EQ}\big(#1;#2\big)}
\newcommand{\ite}[3]{\textsf{if }#1\textsf{ then }#2\textsf{ else }#3}
\newcommand{\itne}[2]{\textsf{if }#1\textsf{ then }#2}
\newcommand{\iteb}[3]{\begin{array}{l}\textsf{if}\: #1 \\ \textsf{then}\: #2 \\ \textsf{else}\: #3\end{array}}
\newcommand{\iteunder}[0]{\texttt{if}\_\texttt{then}\_\texttt{else}\_\xspace}
\newcommand{\xor}{\oplus}
\newcommand{\bool}{\textsf{bool}}
\newcommand{\true}{\textcolor{magenta}{\textsf{true}}}
\newcommand{\combine}{\mathsf{c}}
\newcommand{\pair}[2]{\left\langle #1 \, , \, #2 \right\rangle}
\newcommand{\ipair}[2]{\langle #1 \, , \, #2 \rangle}
\newcommand{\bigpair}[2]{\big\langle #1, #2 \big\rangle}
\newcommand{\Bigpair}[2]{\Big\langle #1, #2 \Big\rangle}
% Encryptions
\newcounter{encnonce}
\newcommand{\enca}[1]{\left\{#1\right\}_{pk_A}^{r_\theencnonce} \stepcounter{encnonce}}
\newcommand{\encb}[1]{\left\{#1\right\}_{pk_B}^{r_\theencnonce} \stepcounter{encnonce}}
\newcommand{\nencb}[2]{\left\{#1\right\}_{pk_B}^{r_{#2}}}
\newcommand{\nenca}[2]{\left\{#1\right\}_{pk_A}^{r_{#2}}}
\newcommand{\tnencb}[2]{\left\{#1\right\}_{pk_B}^{r_{#2}'}}
\newcommand{\tnenca}[2]{\left\{#1\right\}_{pk_A}^{r_{#2}'}}
\newcommand{\enc}[3]{\left\{#1\right\}_{#2}^{#3}}
\newcommand{\nnencb}[2]{\left\{#1\right\}_{pk_B}}
\newcommand{\nnenca}[2]{\left\{#1\right\}_{pk_A}}
\newcommand{\pk}{\textsf{pk}}
\newcommand{\bigenc}[3]{\big\{#1\big\}_{#2}^{#3}}
\newcommand{\Bigenc}[3]{\Big\{#1\Big\}_{#2}^{#3}}
\newcommand{\dec}{\textsf{dec}}
\newcommand{\sk}{\textsf{sk}}
% Math
\newcommand{\Ra}[0]{\Rightarrow}
\newcommand{\la}[2]{\prescript{#1}{#2}{\leftarrow}\,}
\newcommand{\ra}{\rightarrow}
\renewcommand{\Pr}{\mathbf{Pr}}
\newcommand{\prob}{\Pr}
\newcommand{\dom}{\mathsf{dom}}
\newcommand{\rlstep}[2]
{
~\mathop{\mbox{\leftarrowfill}}
\limits^{~{#1}~}_{~{#2}~}~
}
\newcommand{\drawn}[1]{\rlstep{#1}{}}
% Domains
\newcommand{\fresh}[2]{\ensuremath{\textsf{fresh}(#1;#2)}}
\newcommand{\cmodel}{\ensuremath{\mathcal{M}_c}\xspace}
\newcommand{\cdom}{\mathcal{D}}
\newcommand{\sortmessage}{\mathsf{m}}
\newcommand{\names}{\mathsf{names}}
\newcommand{\sem}[1]{[\![#1]\!]}
\newcommand{\term}{\textsf{message}}
\newcommand{\Nonce}{\textsf{nonce}}
% CPRNG
\newcommand{\inits}{\textsf{init}_S}
\newcommand{\cprng}{\textsc{prng}\xspace}
%\renewcommand{\qedsymbol}{\emph{C'est la ce que doit avouer tout homme qui sait qu'une raison claire est infaillible.}}
% Axioms
\newcommand{\axioms}{\mathcal{A}\xspace}
\newcommand{\sigr}[0]{\ensuremath{\mathit{EqCongr}}\xspace}
\newcommand{\sigrt}[0]{\ensuremath{\mathit{EqCongr_2}}\xspace}
\newcommand{\ccao}[0]{\ensuremath{Enc_{CCA1}}\xspace}
\newcommand{\ccat}[0]{\ensuremath{Enc_{CCA2}}\xspace}
\newcommand{\cs}[0]{{\ensuremath{CaseStudy}}\xspace}
\newcommand{\fa}[0]{\ensuremath{FunApp}\xspace}
\newcommand{\fal}[0]{\ensuremath{FunApp_{leaves}}\xspace}
\newcommand{\duplicate}[0]{\ensuremath{Duplicate}\xspace}
\newcommand{\ifthen}[0]{\ensuremath{If_{then}}\xspace}
\newcommand{\iftru}[0]{\ensuremath{If_{true}}\xspace}
\newcommand{\iffals}[0]{\ensuremath{If_{false}}\xspace}
\newcommand{\elses}{\ensuremath{\textsf{else}^*}}
\newcommand{\hiddenr}{\ensuremath{\mathit{hidden}\text{-}\mathit{rand}}}
\newcommand{\sigite}[0]{\ensuremath{\mathcal{F}}\xspace}
\newcommand{\sig}[0]{\ensuremath{\mathcal{F}_\square}\xspace}
\newcommand{\FF}{\sigite}
\newcommand{\GG}{{\mathcal{G}}}
\newcommand{\NN}{\mathcal{N}}
\newcommand{\warningsign}[0]{\begin{tikzpicture} \draw[red] (0,0) -- (0.5,0.866) -- (1,0) -- (0,0); \node[thick,red] (a) at (0.5,0.35) {$!$};\end{tikzpicture}}
% BussProof
\newcommand{\ax}[1]{\AxiomC{$#1$}}
\newcommand{\uinf}[2]{\RightLabel{$#2$}\UnaryInfC{$#1$}}
\newcommand{\uinfL}[2]{\LeftLabel{$#2$}\UnaryInfC{$#1$}}
\newcommand{\binf}[2]{\RightLabel{$#2$}\BinaryInfC{$#1$}}
\newcommand{\tinf}[2]{\RightLabel{$#2$}\TrinaryInfC{$#1$}}
\newcommand{\qinf}[2]{\RightLabel{$#2$}\QuaternaryInfC{$#1$}}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "slides"
%%% End:
\documentclass[handout]{beamer}
\input{macros-beamer.tex}
\usepackage{graphicx}
\usepackage{xspace}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage[english]{babel}
\usepackage{mathtools}
\usepackage{amsfonts}
\usepackage{amsmath}
\usepackage{amsthm}
\usepackage{stmaryrd}
\usepackage{color}
\usepackage{tikz}
\usepackage{bussproofs}
\usepackage{graphicx}
\usepackage{appendixnumberbeamer}
\usepackage{proof}
\usepackage{mathpartir}
\usetheme{Boadilla}
\tikzset{
invisible/.style={opacity=0},
visible on/.style={alt={#1{}{invisible}}},
alt/.code args={<#1>#2#3}{%
\alt<#1>{\pgfkeysalso{#2}}{\pgfkeysalso{#3}} % \pgfkeysalso doesn't change the path
},
}
\title[The APoCI Tool]{The APoCI Tool}
\author[Adrien Koutsos]{Adrien Koutsos}
\newcommand{\cca}{\textsf{CCA1}\xspace}
\newcommand{\tcca}{\textsf{CCA2}\xspace}
\newcommand{\tnum}[1]{\text{\textcolor{red}{\tiny #1}}}
\newcommand{\smallsquare}{\scalebox{0.6}{$\square$}}
\newcommand{\rs}{R_{\smallsquare}}
\newcommand{\csmb}{\textsf{CS}_{\smallsquare}}
\newcommand{\twobox}{\textsf{2Box}}
\newcommand{\restr}{\textsf{Restr}}
\newcommand{\dup}{\textsf{Dup}}
\renewcommand{\fa}{\textsf{FA}}
\renewcommand{\cs}{\textsf{CS}}
\newcommand{\game}[1]{\textsc{\rmfamily #1}}
% Ugly
% \renewcommand{\enc}[3]{\left\{#1\right\}_{#2}^{}}
\begin{document}
\begin{frame}
\maketitle
\end{frame}
\begin{frame}{Structural Rules}
\begin{block}{Duplicate}
\begin{prooftree}
\ax{\visible<2->{\textcolor{red}{\vec w_l},}x \sim \visible<2->{\textcolor{red}{\vec w_r},} y}
\uinf{\visible<2->{\textcolor{red}{\vec w_l},} x,x \sim \visible<2->{\textcolor{red}{\vec w_r},} y,y}{\dup}
\end{prooftree}
\end{block}
\begin{block}{In the Tool}<2->
W.l.o.g we greedily apply this rule.
\end{block}
\end{frame}
\begin{frame}{Structural Rules}
\begin{block}{Function Application}
\begin{quote}
If you cannot distinguish the arguments, you cannot distinguish the images.
\end{quote}
\begin{prooftree}
\ax{\visible<2->{\textcolor{red}{\vec w_l},}x_1,\dots,x_n \sim \visible<2->{\textcolor{red}{\vec w_r},} y_1,\dots,y_n}
\uinf{\visible<2->{\textcolor{red}{\vec w_l},} f(x_1,\dots,x_n) \sim \visible<2->{\textcolor{red}{\vec w_r},} f(y_1,\dots,y_n)}{\fa}
\end{prooftree}
\end{block}
\begin{block}{In the Tool}<2->
We greedily apply this rule on \textcolor{red}{some} function symbols:
\begin{itemize}[<-+>]
\item W.l.o.g on pairs $\pair{\_}{\_}$.
\item W.l.o.g on adversarial function symbols $g_0,g_1,\dots$
\item But also on $\pi_1,\pi_2,\dots$
\end{itemize}
\end{block}
\end{frame}
\begin{frame}{$\alpha$-Renaming}
\begin{alertblock}{Remark: $\sim$ is not a congruence!}
\textbf{Counter-Example:} $\nonce{} \sim \nonce{}$ and $\nonce{} \sim \noncep{}$, but $\nonce{},\nonce{} \not \sim \nonce{},\noncep{}$.
\end{alertblock}
\begin{block}{Valid $\alpha$-Renaming}<2->
\vspace{-0.5em}
\[n_1,n_2 \sim n_3,n_4\]
\end{block}
\begin{block}{The Rule}<3->
We can soundly apply a substitution:
\[
\infer[\alpha]{
\vec u \sim \vec v
}{
\vec u \sigma \sim \vec v
}
\]
\end{block}
\begin{block}{In the Tool}<4->
We maintain a partial substitution which we augment throughout the proof.
\end{block}
\end{frame}
\begin{frame}{Rewriting}
\begin{block}{Congruence}<2->
If $\eq{u}{v} \sim \true$ then $u$ and $v$ are (almost always) \emph{equal}\\
$\textcolor{red}{\Rightarrow}$ we have a congruence.
\end{block}
\vspace{1em}
\visible<2->{$u = v$ syntactic sugar for $\eq{u}{v} \sim \true$
\begin{block}{Equational Theory}
\begin{itemize}
% \item $\ite{y}{x}{x} = x$
\item $\pi_i \left(\langle x_1,x_2 \rangle\right) = x_i $ \hfill $i \in \{1,2\}$
\item $\dec(\enc{x}{\pk(\agent{y})}{z},\sk(\agent{y})) = x$
\end{itemize}
\end{block}
}
\end{frame}
\begin{frame}{Rewriting}
\begin{block}{Rules of the If Then Else}
\(\displaystyle
\begin{array}{l}
\visible<1->{\lefteqn{\textbf{If Homomorphism:}}\\
\begin{array}{lr}
\lefteqn{f(\vec{u},\ite{b}{\textcolor{red}{x}}{\textcolor{blue}{y}},\vec v) = \ite{b}{f(\vec{u},\textcolor{red}{x},\vec v)}{f(\vec{u},\textcolor{blue}{y},\vec v)}} \\
\lefteqn{\ite{(\ite{b}{a}{c})}{\textcolor{red}{x}}{\textcolor{blue}{y}} =} \\
&\qquad \ite{b}{(\ite{a}{\textcolor{red}{x}}{\textcolor{blue}{y}})}{(\ite{c}{\textcolor{red}{x}}{\textcolor{blue}{y}})}
\end{array}}\\[1em]
\visible<2->{\lefteqn{\textbf{If Rewriting:}}\\
\begin{array}{l}
\ite{b}{\textcolor{red}{x}}{\textcolor{red}{x}} = \textcolor{red}{x} \\
\ite{b}{(\ite{b}{\textcolor{red}{x}}{\textcolor{blue}{y}})}{\textcolor{goodgreen}{z}} = \ite{b}{\textcolor{red}{x}}{\textcolor{goodgreen}{z}}\\
\ite{b}{\textcolor{red}{x}}{(\ite{b}{\textcolor{blue}{y}}{\textcolor{goodgreen}{z}})} = \ite{b}{\textcolor{red}{x}}{\textcolor{goodgreen}{z}}
\end{array}}\\[1.5em]
\visible<3->{\lefteqn{\textbf{If Re-Ordering:}}\\
\begin{array}{lr}
\lefteqn{\ite{b}{(\ite{a}{\textcolor{red}{x}}{\textcolor{blue}{y}})}{\textcolor{goodgreen}{z}} =}\\
& \qquad\ite{a}{(\ite{b}{\textcolor{red}{x}}{\textcolor{goodgreen}{z}})}{(\ite{b}{\textcolor{blue}{y}}{\textcolor{goodgreen}{z}})} \\
\lefteqn{\ite{b}{\textcolor{red}{x}}{(\ite{a}{\textcolor{blue}{y}}{\textcolor{goodgreen}{z}})} =}\\
& \qquad\ite{a}{(\ite{b}{\textcolor{red}{x}}{\textcolor{blue}{y}})}{(\ite{b}{\textcolor{red}{x}}{\textcolor{goodgreen}{z}})}
\end{array}}
\end{array}\)
\end{block}
\end{frame}
\begin{frame}{Rewriting}
Luckily, we have a convergent theory.
\begin{block}{Theorem}
There exists a term rewriting system $\ra_R \; \subseteq\; =$ such that:
\begin{itemize}
\item $\ra_R$ is convergent.
\item $=$ is equal to $(\la{}{R} \cup \ra_R)^*$.
\end{itemize}
\end{block}
\begin{block}{In the Tool}<2->
Therefore:
\begin{itemize}
\item We can provide a rewrite rule to the user (and automatically check for validity its applications).
\item Automatic \textcolor{red}{partial} normalization (only rules making the terms smaller).
\end{itemize}
\end{block}
\end{frame}
\begin{frame}{Function Application, Again}
\begin{block}{Function Application Below If Then Elses}
\[
\infer[\fa]{
\ite{b}
{\pair{\textcolor{red}{s_1}}{\textcolor{red}{t_1}}}
{\pair{\textcolor{red}{u_1}}{\textcolor{red}{v_1}}}
\sim
\ite{b}
{\pair{\textcolor{red}{s_2}}{\textcolor{red}{t_2}}}
{\pair{\textcolor{red}{u_2}}{\textcolor{red}{v_2}}}
}{
\begin{alignedat}{2}
&\ite{b}{\textcolor{red}{s_1}}{\textcolor{red}{u_1}},
\ite{b}{\textcolor{red}{t_1}}{\textcolor{red}{v_1}}\\
\sim\;\;&
\ite{b}{\textcolor{red}{s_2}}{\textcolor{red}{u_2}},
\ite{b}{\textcolor{red}{t_2}}{\textcolor{red}{v_2}}
\end{alignedat}
}
\]
\end{block}
\end{frame}
\begin{frame}{Cryptographic Assumptions}
\begin{block}{$Enc_{\cca}$ Games:}<1->
\[
\vec{v},\enc{\textcolor{red}{m_0}}{\pk}{r}
\sim
\vec{v},\enc{\textcolor{red}{m_1}}{\pk}{r'}
\]
\visible<2->{\vspace{-1.5em}
\begin{itemize}
\item $\sk$ occurs only in decryption position in $\vec{v},m_0,m_1$.
\item $r,r'$ do not appear in $\vec{v},m_0,m_1$.
\end{itemize}}
\end{block}
\begin{block}{$Enc_{\tcca}$ Games:}<3->
\[
\begin{alignedat}[t]{2}
&\vec{v},\enc{\textcolor{red}{m_0}}{\pk}{r},
\begin{alignedat}[t]{2}
\ite{t[\enc{\textcolor{red}{m_0}}{\pk}{r}] =
\enc{\textcolor{red}{m_0}}{\pk}{r}&}
{0\\ &}{\dec(t[\enc{\textcolor{red}{m_0}}{\pk}{r}],\sk)}
\end{alignedat}\\
\sim\;\;&
\vec{v},\enc{\textcolor{red}{m_1}}{\pk}{r},
\begin{alignedat}[t]{2}
\ite{t[\enc{\textcolor{red}{m_1}}{\pk}{r}] =
\enc{\textcolor{red}{m_1}}{\pk}{r}&}
{0\\ &}{\dec(t[\enc{\textcolor{red}{m_1}}{\pk}{r}],\sk)}
\end{alignedat}
\end{alignedat}
\]
\visible<4->{
\vspace{-1.5em}
\begin{itemize}
\item Almost the same constraints.
\end{itemize}}
\end{block}
\end{frame}
\begin{frame}{Cryptographic Assumptions}
\begin{block}{Partial Applications}
\begin{itemize}
\item Public/private key pairs.
\item Encryption randomness.
\item Encryption pairs.
\item \emph{And the $\alpha$-renaming.}
\end{itemize}
\end{block}
\begin{block}{In the Tool}<2->
\begin{itemize}
\item Automatic application with a greedy algorithm.
\item Tries to give feedback to the user:
\begin{itemize}
\item Bad encryption randomness.
\item Unguarded decryptions.
\end{itemize}
\item<3-> \textcolor{red}{Actually, we automatically add guards.}
\end{itemize}
\end{block}
\end{frame}
\begin{frame}
\begin{center}
\includegraphics[width=0.8\linewidth]{obi-wan.jpeg}
\textbf{\Large Demonstration of the tool}
\end{center}
\end{frame}
\begin{frame}{The APoCI Tool}
\begin{block}{Organization}
\begin{itemize}
\item 7639 total
\item \textcolor<2->{red}{1741 interactive.ml}
\item \textcolor<2->{blue}{1454 term.ml}
\item 1111 process.ml
\item \textcolor<2->{red}{1050 unitary/cca.ml}
\item 544 rule.ml
\item 500 state.ml
\item 413 formula.ml
\item 298 main.ml
\item 158 axiom\_result.ml
\item 122 unitary/alpha.ml
\item \dots
\end{itemize}
\end{block}
\end{frame}
\end{document}
......@@ -173,7 +173,7 @@ let new_screen state =
Formula.print_formula state.c_proof.goal state.param;
(* Print errors *)
print_separator state.param.shell_mode;
print_separator Param.(state.param.shell_mode);
Printf.printf "\n%!";
state.error_message ();
......@@ -189,7 +189,7 @@ let new_screen state =
(* In shell mode, if the formula is too big we add a new line to avoid
overlapping the input box with the formula. *)
if state'.param.shell_mode then
if Param.(state'.param.shell_mode) then
begin
let (_,h) = ANSITerminal.size () in
......@@ -308,7 +308,7 @@ let is_included compare l l' =
param.small_size_heuristic. *)
let small_size_heuristic state s =
term_size state.c_proof.goal.env s
<= state.param.small_size_heuristic
<= Param.(state.param.small_size_heuristic)
(* apply_ift_heuristic state constraints s t : Use some heuristics to determine
whether we should apply the IfThen axiom to rewrite occurrences of t into s.
......@@ -909,7 +909,7 @@ let cca_auto_guard state sk fk =
| _ -> false end
| _ -> false in
let (l_g_decs,r_g_decs) = List.split constr.decryptions in
let (l_g_decs,r_g_decs) = List.split Cca.(constr.decryptions) in
(* Return true if t is a decryption oracle call. *)
let not_in_g_dec decs t =
......@@ -1292,8 +1292,8 @@ add_s_action
pr_term "v")
(fun ppf () ->
Fmt.pf ppf "rewrite in terms on side %a (\"%a\", \"%a\" or both) at \
positions %a all subterm %a into %a, under the condition that \
Fmt.pf ppf "rewrite in terms on side %a (\"%a\", \"%a\" or both) at@ \
positions %a all subterm %a into %a, under the condition that@ \
%a =_R %a"
pr_side "side" pr_side "l" pr_side "r"
pr_pos "pos"
......@@ -1696,10 +1696,10 @@ let rec interactive_loop state sk fk =
Printf.printf "> %!";
let input_string =
if state'.param.shell_mode then
if Param.(state'.param.shell_mode) then
get_user_input state'
else
try input_line state'.param.input_channel with
try input_line Param.(state'.param.input_channel) with
| End_of_file -> raise Proof_failed in
let (state'',input_commands) =
......
......@@ -114,7 +114,7 @@ let main_interactive () =
let test_state = State.dummy_state ();;
let env =
let env = test_state.c_proof.goal.env in
let env = State.(test_state.c_proof.goal.env) in
List.fold_left (fun env (s,tt) -> bind_type env s tt)
env
......
......@@ -84,11 +84,11 @@ let parse_terms state s =
let _ = Debug.debug (fun () ->
Printf.eprintf "Parsed %d terms:\n" (List.length l_res);
List.iter (fun term ->
(Term.print_term_stderr state.c_proof.goal.env) term;
(Term.print_term_stderr Formula.(state.c_proof.goal.env)) term;
Printf.eprintf "\n%!")
l_res) in
List.map (set_binded_names state.c_proof.goal.env) l_res
List.map (set_binded_names Formula.(state.c_proof.goal.env)) l_res
with
| Term_lexer.Lexer_Error (i) ->
......@@ -124,11 +124,11 @@ let parse_b_terms state s =
let _ = Debug.debug (fun () ->
Printf.eprintf "Parsed %d terms:\n" (List.length l_res);
List.iter (fun term ->
(Term.print_term_stderr state.c_proof.goal.env) term;
(Term.print_term_stderr Formula.(state.c_proof.goal.env)) term;
Printf.eprintf "\n%!")
l_res) in
List.map (set_binded_names state.c_proof.goal.env) l_res
List.map (set_binded_names Formula.(state.c_proof.goal.env)) l_res
with
| Term_lexer.Lexer_Error i ->
......
......@@ -20,9 +20,13 @@ let processB kB pkA nB s =
out(cB,s);
let P_L =
new kA.new kB.out(c,pk(kA)).out(c,pk(kB)).(processA kA (pk(kB)) | (new nB.processB kB (pk(kA)) nB nB));
new kA.new kB.out(c,pk(kA)).out(c,pk(kB)).
(processA kA (pk(kB))
| (new nB.processB kB (pk(kA)) nB nB));
let P_R =
new kA.new kB.out(c,pk(kA)).out(c,pk(kB)).(processA kA (pk(kB)) | (new nB.new s.processB kB (pk(kA)) nB s));
new kA.new kB.out(c,pk(kA)).out(c,pk(kB)).
(processA kA (pk(kB))
| (new nB.new s.processB kB (pk(kA)) nB s));
goal: P_L ~ P_R
\ No newline at end of file
(* First trace *)
obiwan;
cca2;
help;
fab 7;
cca2 guard;
cca2 guard;
cond_fresh Left EQ(<nA_l,A()>,nB_l);
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment