text:
\section{Introduction}

One of the fundamental aspects of the analysis of security protocols is the model
of the intruder that seeks to compromise the protocols. In many situations,
such a model can be described in terms of a deduction system which gives a formal
account of the ability of the intruder to analyse and synthesize messages.
As shown in many previous works
(see, e.g., ~\cite{Amadio00CONCUR,Boreale01ICALP,Comon-Lundh03LICS,Chevalier03LICS}),
finding attacks on protocols can often be framed as
the problem of deciding whether a certain formal expression is derivable in
the deduction system which models the intruder capability. The latter is sometimes called
the {\em intruder deduction problem}, or the (ground) reachability problem.
A basic deductive account of the intruder's capability
is based on the so-called Dolev-Yao model, which assumes perfect encryption.
While this model has been applied fruitfully to many situations,
a stronger model of intruders is needed to discover certain types of attacks.
A recent survey \cite{Cortier06JCS} shows that attacks on several protocols used in real-world communication
networks can be found by exploiting algebraic properties of
encryption functions.

The types of attacks mentioned in \cite{Cortier06JCS} have motivated
many recent works in studying models of intruders in which the
algebraic properties of the operators used in the protocols are taken
into
account~\cite{Comon-Lundh03LICS,Chevalier03LICS,Abadi06TCS,Delaune06ICALP,Lafourcade07IC,Cortier07LPAR}.
In most of these, the intruder's capability is usually given as
a natural-deduction-like deductive system. As is common in natural
deduction, each constructor has a rule for introducing the constructor and
one for eliminating the constructor.
The elimination rule typically decomposes a term, reading
the rule top-down: {\em e.g.}, a typical elimination rule for a pair
$\spr M N$ of terms is:
$$
\infer[]
{\Gamma \vdash M}
{\Gamma \vdash \spr M N}
$$
Here, $\Gamma$ denotes a set of terms, which represents the terms
accumulated by the intruder over the course of its interaction with
participants in a protocol. While a natural deduction formulation of
deductive systems may seem ``natural'' and may reflect the meaning of
the (logical) operators, it does not immediately give us a proof
search strategy. Proof search means that we have to apply the rules
bottom up, and as the above elimination rule demonstrates, this
requires us to come up with a term $N$ which might seem arbitrary.
For a more complicated example, consider the following elimination
rule for {\em blind signatures} \cite{Fujioka92,KremerESOP05,Bernat06}.
$$
\infer[]
{\Gamma \vdash \sign M K}
{\Gamma \vdash \sign {\blind M R} K & \Gamma \vdash R}
$$
The basis for this rule is that the ``unblinding'' operation commutes
with signature.  Devising a proof search strategy in a natural
deduction system containing this type of rule does not seem trivial.
In most of the works mentioned above, in order to show the
decidability results for the natural deduction system, one needs to
prove that the system satisfies a notion of {\em locality}, i.e., in
searching for a proof for $\Gamma \vdash M$, one needs only to
consider expressions which are made of subterms from $\Gamma$ and $M.$
In addition, one has to also deal with the complication that arises
from the use of the algebraic properties of certain operators.

In this work, we recast the intruder deduction problem as proof search
in sequent calculus. A sequent calculus formulation of Dolev-Yao
intruders was previously used by the first author in a formulation of
open bisimulation for the spi-calculus~\cite{Tiu07APLAS} to prove
certain results related to open bisimulation.  The current work takes
this idea further to include richer theories.  Part of our motivation
is to apply standard techniques, which have been well developed in the
field of logic and proof theory, to the intruder deduction problem. In
proof theory, sequent calculus is commonly considered a better
calculus for studying proof search and decidability of logical
systems, in comparison to natural deduction. This is partly due to the
so-called ``subformula'' property (that is, the premise of every
inference rule is made up of subterms of the conclusion of the rule),
which in most cases entails the decidability of the deductive
system. It is therefore rather curious that none of the existing works
on intruder deduction so far uses sequent calculus to structure proof
search.  We consider the ground intruder deduction problem (i.e.,
there are no variables in terms) under the class of {\em AC-convergent
  theories}. These are equational theories that can be turned into
convergent rewrite systems, modulo associativity and commutativity of
certain binary operators. Many important theories for intruder
deduction fall into this category, e.g., theories for
exclusive-or~\cite{Comon-Lundh03LICS,Chevalier03LICS}, Abelian
groups~\cite{Comon-Lundh03LICS}, and more generally, certain classes
of monoidal theories~\cite{Cortier07LPAR}.

We show two main results.
Firstly, we show that the
decidability of intruder deduction under AC-convergent theories can be
reduced, in polynomial time,
to {\em elementary intruder deduction problems}, which involve
only the equational theories under consideration.
Secondly, we show that the intruder deduction problem for a
combination of disjoint theories $E_1,\ldots,E_n$ can be reduced, in polynomial time,
to the elementary deduction problem {\em for each theory $E_i$.} This
means that if the elementary deduction problem is decidable for each
$E_i$, then the intruder deduction problem under the combined theory
is also decidable.
We note that these decidability results are not really new,
although there are slight differences and improvements over the
existing works (see Section~\ref{sec:rel}).
Our contribution is more of a methodological nature. We
arrive at these results using rather standard proof theoretical
techniques, e.g., {\em cut-elimination} and permutability of inference
rules, in a uniform and systematic way. In particular, we obtain
locality of proof systems for intruder deduction, which is one of the
main ingredients to decidability results in
\cite{Comon-Lundh03LICS,Chevalier03LICS,Delaune06ICALP,Delaune06IPL},
for a wide range of theories that cover those studied in these works.
Note that these works deal with a more difficult problem of deducibility
constraints, which models {\em active intruders}, whereas we currently
deal only with passive intruders.  As future work, we plan to
extend our approach to deal with active intruders.

The remainder of the paper is organised as follows.
Section~\ref{sec:intruder} presents two systems for intruder theories,
one in natural deduction and the other in sequent calculus, and show that the two systems are equivalent.
In Section~\ref{sec:cutelim}, the sequent system is shown to enjoy cut-elimination.
In Section~\ref{sec:normal}, we show that cut-free sequent derivations can be transformed into a certain
normal form. Using this result, we obtain another ``linear'' sequent system, from which the polynomial
reducibility result follows. Section~\ref{sec:examples} discusses several example theories
which can be found in the literature. Section~\ref{sec:comb} shows that the sequent system
in Section~\ref{sec:intruder} can be extended to cover any combination of disjoint AC-convergent theories,
and the same decidability results also hold for this extension.
Detailed proofs can be found in the appendix.

\section{Intruder deduction under AC convergent theories}
\label{sec:intruder}

We consider the following problem of formalising, given a set of messages
$\Gamma$ and a message $M$, whether $M$ can be synthesized from the messages
in $\Gamma.$ We shall write this judgment as $\Gamma \vdash M.$ This is sometimes called
the `ground reachability' problem or the `intruder deduction' problem in the literature.

Messages are formed from names, variables and function symbols.  We
shall assume the following sets: a countably infinite set $\mathsf{N}$
of names ranged over by $a$, $b$, $c$, $d$, $m$ and $n$; a countably
infinite set $\mathsf{V}$ of variables ranged over by $x$, $y$ and $z$;
and a finite set $\Sigma_C = \{\mathsf{pub}, \mathsf{sign}, \mathsf{blind},
\spr{.}{.}, \enc{.}{.}\}$ of symbols representing the {\em
  constructors}. Thus $ \mathsf{pub}$ is a public key constructor,
$\mathsf{sign}$ is a public key encryption function, $\mathsf{blind}$ is the
blinding encryption function (as in
\cite{Fujioka92,KremerESOP05,Bernat06}), $\spr{.}{.}$ is a pairing
constructor, and $\enc{.}{.}$ is the Dolev-Yao symmetric encryption
function.  Additionally, we also assume a possibly empty equational
theory $E$, whose signature is denoted with $\Sigma_E.$ We require
that $\Sigma_C \cap \Sigma_E = \emptyset.$\footnote{This restriction
means that intruder theory such as homomorphic encryption is excluded.
Nevertheless, it still covers a wide range of intruder theories.}
Function symbols (including
constructors) are ranged over by $f$, $g$ and $h$.  The equational
theory $E$ may contain at most one associative-commutative function
symbol, which we denote with $\oplus$, obeying the standard
associative and commutative laws.  We restrict ourselves to equational
theories which can be represented by terminating and confluent rewrite
systems, modulo the associativity and commutativity of $\oplus.$ We
consider the set of messages generated by the following grammar
$$
\begin{array}{ll}
M, N := & a \mid x \mid \pub M \mid \sign M N \mid \blind M N
\\      & \;\;\; \mid \spr M N \mid \enc M N \mid f(M_1,\ldots,M_k).
\end{array}
$$
The message $\pub M$ denotes the public key generated from a private key $M$;
$\sign M N$ denotes a message $M$ signed with a private key $N$;
$\blind M N$ denotes a message $M$ encrypted with $N$ using a
special blinding encryption; $\spr M N$ denotes a pair of messages;
and $\enc M N$ denotes a message $M$ encrypted with a key $N$ using
a Dolev-Yao symmetric encryption.
The blinding encryption has a special property that it commutes with
the $\mathsf{sign}$ operation, i.e., one can ``unblind'' a signed blinded
message $\sign {\blind M r} k$ using the blinding key $r$
to obtain $\sign M k.$ This aspect of the blinding encryption is
reflected in its elimination rules, as we shall see later.
We denote with $V(M)$ the set of variables occurring in $M$. A term $M$ is {\em ground}
if $V(M) = \emptyset.$
We shall be mostly concerned with ground terms, so unless
stated otherwise, we assume implicitly that terms are ground (the only exception
is Proposition~\ref{prop:var-abs} and Proposition~\ref{prop:var-abs2}).

We shall use several notions of equality so we distinguish them using the following
notation: we shall write $M = N$ to denote syntactic equality, $M
\equiv N$ to denote equality modulo associativity and commutativity
(AC) of $\oplus$, and $M \approx_T N$ to denote equality modulo a
given equational theory $T$. We shall sometimes omit the subscript in
$\approx_T$ if it can be inferred from context.

Given an equational theory $E$, we denote with $R_E$ the set of
rewrite rules for $E$ (modulo AC). We write $M \to_{R_E} N$ when
$M$ rewrites to $N$ using one application of a rewrite rule in $R_E$. The definition
of rewriting modulo AC is standard and is omitted here.
The reflexive-transitive closure of $\to_{R_E}$  is denoted with $\rightarrow_{R_E}^*.$
We shall often remove the subscript $R_E$ when no confusion arises.
A term $M$ is in {\em $E$-normal form} if $M \not \to_{R_E} N$ for any $N.$
We write $\normE M E$ to denote the normal form of $M$ with respect to
the rewrite system $R_E$, modulo commutativity and associativity of $\oplus$.
Again, the index $E$ is often omitted when it is clear which equational theory we
refer to.
This notation extends straightforwardly to sets, e.g., $\norm \Gamma$ denotes the set obtained
by normalising all the elements of $\Gamma.$
A term $M$ is said to be {\em headed by } a symbol $f$ if $M = f(M_1,\ldots,M_k)$.
$M$ is {\em guarded}
if it is either a name, a variable, or a term headed by a constructor.
A term $M$ is an {\em $E$-alien term} if $M$ is headed by a symbol $f \not \in \Sigma_E.$
It is a {\em pure $E$-term} if it contains only symbols from $\Sigma_E$, names and variables.

A {\em context} is a term with holes. We denote with $C^k[]$ a context with $k$-hole(s).
When the number $k$ is not important or can be inferred from context, we shall write
$C[\ldots]$ instead. Viewing a context $C^k[]$ as a tree, each hole in the context
occupies a unique position among the leaves of the tree. We say that a hole occurrence
is the $i$-th hole of the context $C^k[]$ if it is the $i$-th hole encountered in
an inorder traversal of the tree representing $C^k[].$
An $E$-context is a context formed using only the function symbols in $\Sigma_E.$
We write $C[M_1,\ldots,M_k]$ to denote the term resulting
from replacing the holes in the $k$-hole context $C^k[]$ with $M_1, \ldots, M_k,$
with $M_i$ occuping the $i$-th hole in $C^k[].$

\paragraph{Natural deduction and sequent systems}

The standard formulation of the judgment $\Gamma \vdash M$ is usually given in
terms of a natural-deduction style inference system, as shown in
Figure~\ref{fig:nat}. We shall refer to this proof system as ${\cal N}$
and write $\Gamma \Vdash_{\cal N} M$ if $\Gamma \vdash M$ is derivable in ${\cal N}.$
The deduction rules for Dolev-Yao encryption is standard and can be found
in the literature, e.g., \cite{Boreale01ICALP,Comon-Lundh03LICS}.
The blind signature rules are taken from the formulation given by Bernat and
Comon-Lundh~\cite{Bernat06}. Note that the rule $\mathsf{sign}_E$ assumes
implicitly that signing a message hides its contents. An alternative rule
without this assumption would be
$$
\infer[]
{\Gamma \vdash M}
{\Gamma \vdash \sign M K}
$$
The results of the paper also hold, with minor modifications, if we adopt this rule.

\begin{figure}[t]
  \begin{tabular}[c]{l@{\extracolsep{0.8cm}}ll}
    $\infer[id]{\Gamma \vdash M}
               {M \in \Gamma}$
  & $\infer[e_E]{\Gamma \vdash M}
                {\Gamma \vdash \enc M K & \Gamma \vdash K}$
  & $\infer[e_I]{\Gamma \vdash \enc M K}
                {\Gamma \vdash M & \Gamma \vdash K}$
\\[1em]
    $\infer[p_E]{\Gamma \vdash M}
                {\Gamma \vdash \spr M N}$
  & $\infer[p_E]{\Gamma \vdash N}
                {\Gamma \vdash \spr M N}$
  & $\infer[p_I]{\Gamma \vdash \spr M N}
                {\Gamma \vdash M & \Gamma \vdash N}$
\\[1em]
  \multicolumn{2}{c}{
      $\infer[\mathsf{sign}_E]{\Gamma \vdash M}
                         {\Gamma \vdash \sign M K & \Gamma \vdash \pub K}$
    }
  &  $\infer[\mathsf{sign}_I]{\Gamma \vdash \sign M K}
                       {\Gamma \vdash M & \Gamma \vdash K}$
\\[1em]
    \multicolumn{2}{c}{
    $\infer[\mathsf{blind}_{E1}]{\Gamma \vdash M}
                          {\Gamma \vdash \blind M K & \Gamma \vdash K}$
    }
  &
    $\infer[\mathsf{blind}_I]{\Gamma \vdash \blind M K}
                        {\Gamma \vdash M & \Gamma \vdash K}$
\\[1em]
    \multicolumn{3}{c}{
     $\infer[\mathsf{blind}_{E2}]{\Gamma \vdash \sign M K}
                       {\Gamma \vdash \sign {\blind M R} K & \Gamma \vdash R}$
    }
\\[1em]
    \multicolumn{2}{c}{
    $\infer[f_I, \hbox{ where } f \in \Sigma_E]
           {\Gamma \vdash f(M_1,\ldots,M_n)}
           {\Gamma \vdash M_1 & \cdots & \Gamma \vdash M_n}$
    }
  &
    \multicolumn{1}{c}{
    $\infer[\approx, \hbox{ where $M \approx_{E} N$}]
                          {\Gamma \vdash M}
                          {\Gamma \vdash N}$
    }
  \end{tabular}
\caption{System ${\cal N}$: a natural deduction system for intruder deduction}
\label{fig:nat}
\end{figure}

A sequent $\Gamma \vdash M$ is in {\em normal form} if $M$ and all the terms in $\Gamma$ are
in normal form. Unless stated otherwise, in the following we assume that sequents
are in normal form.
The sequent system for intruder deduction, under the equational theory $E$,
is given in Figure~\ref{fig:msg}. We refer to this sequent system as ${\cal S}$
and write $\Gamma \Vdash_{\cal S} M$ to denote the fact that the sequent
$\Gamma \vdash M$ is derivable in ${\cal S}.$

Unlike natural deduction rules, sequent rules also allow introduction of terms on
the left hand side of the sequent.
The rules $p_L,$ $e_L,$ $\mathsf{sign}_L,$ $\mathsf{blind}_{L1},$ $\mathsf{blind}_{L2},$ and  $gs$ are called
{\em left introduction rules} (or simply {\em left rules}),
and the rules $p_R, e_R, \mathsf{sign}_R, \mathsf{blind}_R$ are called {\em right introduction
rules} (or simply, {\em right rules}).
Notice that the rule $gs$ is very similar to $cut$, except that we have the
proviso that $A$ is a subterm of a term in the lower sequent. This is sometimes
called {\em analytic cut} in the proof theory literature. Analytic cuts are
not problematic as far as proof search is concerned, since it still obeys the
sub-formula property.

We need the rule $gs$ because we do not have introduction rules for
function symbols in $\Sigma_E$, in contrast to natural deduction. This
rule is needed to ``abstract'' $E$-alien subterms in a sequent (in the
sense of the variable abstraction technique common in unification theory, see
e.g., \cite{Schmidt-Schauss89,Baader96JSC}), which is needed to prove
that the cut rule is redundant.  For example, let $E$ be a theory containing
only the associativity and the commutativity axioms for $\oplus$.
Then the sequent ~ $ a, b \vdash
\spr a b \oplus a $ should be provable without cut. Apart from the
$gs$ rule, the only other way to prove this is by using the $id$
rule. However, $id$ is not applicable, since no $E$-context
$C[...]$ can obey $C[a,b] \approx
\spr a b \oplus a$
because
$E$-contexts can contain only symbols from
$\Sigma_E$ and thus cannot contain $\spr . .$.
Therefore we need to ``abstract'' the term $\spr a
b$ in the right hand side, via the $gs$ rule:
$$
\infer[gs]
{a, b \vdash \spr a b \oplus a}
{
  \infer[p_R]
  {a, b \vdash \spr a b}
  {\infer[id]{a,b\vdash a}{} & \infer[id]{a,b \vdash b}{}}
 &
  \infer[id]
  {a, b, \spr a b \vdash \spr a b \oplus a}
  {}
}
$$
The third $id$ rule instance (from the left) is valid because we have
$C[\spr a b, a] \equiv \spr a b \oplus a$, where
$C[.,.] = [.] \oplus [.].$

\begin{figure}[t]
  \begin{tabular}[c]{ll}
   $\infer[id]{\Gamma \vdash M}
              {
              \begin{array}{c}
               M \approx_{E} C[M_1,\ldots,M_k] \\
                \hbox{$C[\ ]$ an $E$-context, and $M_1,\ldots,M_k \in \Gamma$}
              \end{array}
              }$
  & $\infer[cut]{\Gamma \vdash T}
                {\Gamma \vdash M
                 & \Gamma, M \vdash T}$
\\[1em]
  $\infer[p_L]{\Gamma, \spr M N \vdash T}
              {\Gamma, \spr M N, M, N \vdash T}$
  & $\infer[p_R]{\Gamma \vdash \spr M N}
                {\Gamma \vdash M & \Gamma \vdash N}$
\\[1em]
  $\infer[e_L]{\Gamma, \enc M K \vdash N}
              {\Gamma, \enc M K \vdash K
                & \Gamma, \enc M K, M, K \vdash N}$
  & $\infer[e_R]{\Gamma \vdash \enc M K}
                {\Gamma \vdash M & \Gamma \vdash K}$
\\[1em]
  $\infer[\mathsf{sign}_L, K \equiv L]{\Gamma, \sign M K, \pub L \vdash N}
                                 {\Gamma, \sign M K, \pub L, M \vdash N}$
  & $\infer[\mathsf{sign}_R]{\Gamma \vdash \sign M K}
                       {\Gamma \vdash M & \Gamma \vdash K}$
\\[1em]
  $\infer[\mathsf{blind}_{L1}]{\Gamma, \blind M K \vdash N}
                        {\Gamma, \blind M K \vdash K
                         & \Gamma, \blind M K, M, K \vdash N}$
  & $\infer[\mathsf{blind}_R]{\Gamma \vdash \blind M K}
                       {\Gamma \vdash M & \Gamma \vdash K}$
\\[1em]
  \multicolumn{2}{c}{
    $\infer[\mathsf{blind}_{L2}]{\Gamma, \sign {\blind M R} K \vdash N}
                          {\Gamma, \sign {\blind M R} K \vdash R
                           &
                           \Gamma, \sign {\blind M R} K, \sign M K, R \vdash N}$
  }
\\[1em]
  \multicolumn{2}{c}{
   $\infer[gs, \hbox{$A$ is a guarded subterm of $\Gamma \cup \{M\}$}]
           {\Gamma \vdash M}
           {\Gamma \vdash A & \Gamma, A \vdash M}$
  }
\end{tabular}
\caption{System ${\cal S}$: a sequent system for intruder deduction. }
\label{fig:msg}
\end{figure}

Provability in the natural deduction system and in the sequent system
are related via the standard translation, i.e., right rules in sequent calculus
correspond to introduction rules in natural deduction and left rules corresponds
to elimination rules. The straightforward
translation from natural deduction to sequent calculus uses the cut rule.

\begin{proposition}
\label{prop:S-equal-N}
The judgment $\Gamma \vdash M$ is provable in the natural deduction system ${\cal N}$
if and only if $\norm \Gamma \vdash \norm M$ is provable in the sequent system ${\cal S}$.
\end{proposition}

\section{Cut elimination for ${\cal S}$}
\label{sec:cutelim}

We now show that the cut rule is redundant for ${\cal S}$.
\begin{definition}
An inference rule $R$ in a proof system ${\cal D}$ is {\em admissible for ${\cal D}$} if
for every sequent $\Gamma \vdash M$ derivable in ${\cal D}$, there is a derivation
of the same sequent in ${\cal D}$ without instances of $R$.
\end{definition}
The {\em cut-elimination} theorem for ${\cal S}$
states that the cut rule is admissible for ${\cal S}$. Before we proceed
with the main cut elimination proof, we first prove a basic property
of equational theories and rewrite systems, which is concerned with a
technique called {\em variable abstraction} \cite{Schmidt-Schauss89,Baader96JSC}.

Given derivation $\Pi$, the {\em height} of the derivation, denoted by $|\Pi|$,
is the length of a longest branch in $\Pi.$ Given a normal term $M$,
the {\em size} $|M|$ of $M$ is the number of function
symbols, names and variables appearing in $M.$

In the following, we consider slightly more general equational
theories than in the previous section:
each $AC$ theory $E$ can be a theory obtained from a disjoint combination of
$AC$ theories $E_1, \ldots, E_k$, where each $E_i$ has at most
one AC operator $\oplus_i.$ This allows us to reuse the results for a
more general case later.

\begin{definition}
  Let $E$ be a disjoint combination of AC convergent theories
  $E_1,$ $\dots,$ $E_n$.  A term $M$ is a {\em quasi-$E_i$ term} if every
  $E_i$-alien subterm of $M$ is in $E$-normal form.
\end{definition}

For example, let $E = \{h(x,x) \approx x \}$.
Then $h(\spr a b, c)$ is a quasi $E$-term, whereas $h(\spr a b, \spr
{h(a,a)} b)$ is not, since its $E$-alien subterm $\spr {h(a,a)} b$ is not
in its $E$-normal form $\spr{a}{b}$. Obviously, any $E$ normal term is a quasi $E_i$ term.

In the following, given an equational theory $E$, we assume the
existence of a function $v_E$, which assigns a variable from $\mathsf{V}$
to each ground term such that $v_E(M) = v_E(N)$ if and only if $M
\approx_E N.$ In other words, $v_E$ assigns a unique variable to each
equivalence class of ground terms induced by $\approx_E.$

\begin{definition}
Let $E$ be an equational theory obtained by disjoint combination of
AC theories $E_1, \ldots, E_n$.
The {\em $E_i$ abstraction function} $F_{E_i}$ is a function
mapping ground terms to pure $E_i$ terms, defined recursively as follows:
$$
F_{E_i}(u) =
\left\{
\begin{array}{ll}
u, & \hbox{ if $u$ is a name, }\\
f(F_{E_i}(u_1), \ldots, F_{E_i}(u_k)), & \hbox{if $u=f(u_1,\ldots,u_k)$ and $f \in \Sigma_{E_i}$,} \\
v_E(u), & \hbox{ otherwise.}
\end{array}
\right.
$$
\end{definition}

It can be easily shown that the function $F_{E_i}$ preserves the equivalence relation
$\equiv$. That is, if $M \equiv  N$ then $F_{E_i}(M) \equiv F_{E_i}(N)$.

\begin{proposition}
\label{prop:var-abs}
Let $E$ be a disjoint combination of $E_1,\ldots,E_n$.
If $M$ is a quasi $E_i$ term and $M \to^*_{R_E} N$, then
$N$ is a quasi $E_i$ term and $F_{E_i}(M) \to^*_{R_E} F_{E_i}(N).$
\end{proposition}

\begin{proposition}
\label{prop:var-abs2}
Let $E$ be a disjoint combination of $E_1,\ldots,E_n$.
If $M$ and $N$ are quasi $E_i$ terms and
$F_{E_i}(M) \to^*_{R_E} F_{E_i}(N)$, then
$M \to^*_{R_E} N.$
\end{proposition}

We now show some important proof transformations needed to prove cut elimination,
i.e., in an inductive argument to reduce the size of cut terms.
In the following, when we write that a sequent $\Gamma \vdash M$ is derivable,
we mean that it is derivable in
the proof system ${\cal S}$, with a fixed AC theory $E$.

\begin{lemma}
\label{lm:equiv}
Let $\Pi$ be a derivation of $M_1, \ldots, M_k \vdash N.$ Then for any
$M_1',$ $\ldots,$ $M_k'$ and $N'$
such that $M_i \equiv M_i'$ and $N \equiv N'$, there is a derivation $\Pi'$
of $M_1', \ldots, M_k' \vdash N'$ such that $|\Pi| = |\Pi'|.$
\end{lemma}

\begin{lemma}
\label{lm:decomp1}
Let $X$ and $Y$ be terms in normal form and let $f$ be a binary
constructor.  If $\Gamma, f(X,Y) \vdash M$ is cut-free derivable, then
so is $\Gamma, X, Y \vdash M$.
\end{lemma}

The more interesting case in the proof of Lemma~\ref{lm:decomp1}
is when  $\Gamma, f(X,Y) \vdash M$ is proved by an application of the $id$
rule where $f(X,Y)$ is active. That is, we have
$
C[f(X,Y),M_1, \ldots, M_k] \approx_E M,
$
where $M_1,\dots,M_k \in \Gamma$,
for some $E$-context $C[..].$ Since $M$ is in normal form, we have
\begin{equation}
\label{eq1}
C[f(X,Y), M_1, \ldots, M_k] \rightarrow^* M.
\end{equation}
There are two cases to consider in the construction of a proof for
$\Gamma, X, Y \vdash M.$ If $f(X,Y)$
occurs as a subterm of $M$ or $\Gamma$, then we simply apply the $gs$
rule (bottom up) to abstract the term $f(X,Y)$ and then apply the
$id$ rule.
Otherwise,  we use the variable abstraction techniques
(Proposition~\ref{prop:var-abs} and  Proposition~\ref{prop:var-abs2})
to abstract $f(X,Y)$ from the rewrite steps (\ref{eq1}) above,
and then replace its abstraction with $X$ to obtain:
$
C[X,M_1, \ldots, M_k] \rightarrow^* M.
$
That is, the $id$ rule is applicable to the sequent $\Gamma, X, Y \vdash M$,
with $X$ taking the role of $f(X,Y)$.

\begin{lemma}
\label{lm:decomp2}
Let $X_1,\ldots, X_k$ be normal terms and let
$\Pi$ be a cut-free derivation of $\Gamma, \norm{f(X_1,\ldots,X_k)} \vdash M$, where $f \in \Sigma_E.$
Then there exists a cut-free derivation $\Pi'$ of $\Gamma, X_1,\ldots,X_k \vdash M.$
\end{lemma}

\begin{lemma}
\label{lm:decomp3}
Let $M_1, \ldots, M_k$ be terms in normal form and let $C[\ldots]$ be
a $k$-hole $E$-context. If $\Gamma, \norm{C[M_1,\ldots,M_k]} \vdash M$
is cut-free derivable, then so is $\Gamma, M_1, \ldots, M_k \vdash M$.
\end{lemma}

One peculiar aspect of the sequent system ${\cal S}$ is that in the
introduction rules for encryption functions (including blind
signatures), there is no switch of polarities for the encryption
key. For example, in the introduction rule for $\enc M K$, both on the
left and on the right, the key $K$ appears on the right hand
side of a premise of the rule. This means that there is no exchange
of information between the left and the right hand side of sequents,
unlike, say, typical implication rules in logic. This gives rise to an
easy cut elimination proof, where we need only to measure the
complexity of the left premise of a cut in determining the cut
rank.

\begin{theorem}
\label{thm cut elim}
The cut rule is admissible for ${\cal S}$.
\end{theorem}

\section{Normal derivations and decidability}
\label{sec:normal}

We now turn to the question of the decidability of the deduction problem
$\Gamma \vdash M.$ This problem is known already for several AC theories,
e.g., exclusive-or, abelian groups and their extensions with a homomorphism
axiom~\cite{Comon-Lundh03LICS,Chevalier03LICS,Delaune06ICALP,Delaune06IPL,Abadi06TCS}.
What we would like to show here is how the decidability
result can be reduced to a more elementary decision
problem, defined as follows.

\begin{definition}
Given an equational theory $E$, the {\em elementary deduction problem} for $E$, written $\Gamma \Vdash_E M$,
is the problem of deciding whether the $id$ rule is applicable
to the sequent $\Gamma \vdash M$ (by checking
whether there exists an $E$-context
$C[\ldots]$ and terms $M_1,\ldots, M_k \in \Gamma$ such that
$C[M_1,\ldots,M_k] \approx_{E} M$).
\end{definition}

Note that as a consequence of Proposition~\ref{prop:var-abs} and Proposition~\ref{prop:var-abs2},
in checking elementary deducibility, it is enough to consider the pure $E$ equational
problem where all $E$-alien subterms are abstracted, i.e., we have
$$
C[M_1, \ldots, M_k] \approx_{E} M
\qquad
\mbox{iff}
\qquad
C[F_E(M_1), \ldots, F_E(M_k)] \approx_E F_E(M).
$$
Our notion of elementary deduction corresponds roughly to the notion of ``recipe''
in \cite{Abadi06TCS}, but we note that the notion of a recipe is a stronger one, since it
bounds the size of the equational context.

The cut free sequent system does not strictly speaking enjoy the ``sub-formula'' property,
i.e., in $\mathsf{blind}_{L2}$, the premise sequent has a term which is not a subterm of
any term in the lower sequent. However, it is easy to see that, reading the rules bottom up,
we only ever introduce terms which are smaller than the terms in the lower sequent.
Thus a naive proof search strategy which non-deterministically tries all applicable rules
and avoids repeated sequents will eventually terminate.
This procedure is of course rather expensive.
We show that we can obtain a better complexity result by analysing the structures of cut-free derivations.
Recall that the rules $p_L, e_L, \mathsf{sign}_L, \mathsf{blind}_{L1}, \mathsf{blind}_{L2}$ and $gs$
are called left rules (the other rules are right rules).

\begin{definition}
A cut-free derivation $\Pi$ is said to be a {\em normal derivation} if
it satisfies the following conditions:
\begin{enumerate}
\item no left rule appears above a right rule;
\item no left rule appears immediately above the left-premise of a
  branching left rule (i.e., all left rules except $p_L$ and
  $\mathsf{sign}_L$).
\end{enumerate}
\end{definition}

\begin{proposition}
\label{prop:norm}
If $\Gamma \vdash M$ is derivable then it has a normal derivation.
\end{proposition}

In a normal derivation, the left branch of a branching left rule is
provable using only right rules and $id$. This means that we can
represent a normal derivation as a sequence (reading the proof bottom-up)
of sequents, each of which is obtained from the previous
one by adding terms composed of subterms of the previous sequent, with
the proviso that certain subterms can be constructed using
right-rules.  Let us denote with $\Gamma \Vdash_{\cal R} M$ the fact that
the sequent $\Gamma \vdash M$ is provable using only the right rules
and $id$.  This suggests a more compact deduction system for intruder
deduction, called system ${\cal L}$, given in Figure~\ref{fig:linear}.

\begin{figure}[t]
  \begin{tabular}[c]{ll}
   $\infer[r]{\Gamma \vdash M}
             {\Gamma \Vdash_{\cal R} M}$
  &
   \qquad $\infer[le, \hbox{ where $\Gamma, \enc M K \Vdash_{\cal R} K$}]
              {\Gamma, \enc M K \vdash N}
              {\Gamma, \enc M K, M, K \vdash N}$
\\[1em]
   $\infer[lp]{\Gamma, \spr M N \vdash T}
              {\Gamma, \spr M N, M, N \vdash T}$
   &
   \qquad $\infer[\mathsf{sign}, K \equiv L]
              {\Gamma, \sign M K, \pub L \vdash N}
              {\Gamma, \sign M K, \pub L, M \vdash N}$
\\[1em]
  \multicolumn{2}{l}{
   $\infer[\mathsf{blind}_1, \hbox{ where $\Gamma, \blind M K \Vdash_{\cal R} K$ }]
             {\Gamma, \blind M K \vdash N}
             {\Gamma, \blind M K, M, K \vdash N}$
  }
\\[1em]
  \multicolumn{2}{l}{
   $\infer[\mathsf{blind}_2,]
             {\Gamma, \sign {\blind M R} K \vdash N}
             {\Gamma, \sign {\blind M R} K, \sign M K, R \vdash N}$
  }
\\[1em]
  \multicolumn{2}{l}{\qquad where $\Gamma, \sign {\blind M R} K \Vdash_{\cal R} R.$}
\\[1em]
  \multicolumn{2}{l}{
  $\infer[ls,
           \hbox{where $A$ is a guarded subterm of $\Gamma \cup \{M\}$
                 and $\Gamma \Vdash_{\cal R} A.$}]
            {\Gamma \vdash M}
            {\Gamma, A \vdash M} $
  }
  \end{tabular}
\caption{System ${\cal L}$: a linear proof system for intruder deduction.}
\label{fig:linear}
\end{figure}

\begin{proposition}
\label{prop:normal}
Every sequent $\Gamma \vdash M$ is provable in ${\cal S}$ if and only if it
is provable in ${\cal L}.$
\end{proposition}

We now show that the decidability of the deduction problem $\Gamma \Vdash_{\cal S} M$
can be reduced to decidability of elementary deduction problems.
We consider a representation of terms as directed acyclic graphs (DAG),
with maximum sharing of subterms.
Such a representation is quite standard and can be found in, e.g., \cite{Abadi06TCS}, so
we will not go into the details here.

In the following, we denote with $st(\Gamma)$ the set of subterms of the terms in $\Gamma.$
In the DAG representation of $\Gamma$, the number of distinct nodes in the DAG representing
distinct subterms of $\Gamma$ co-incides with the cardinality of $st(\Gamma).$
A term $M$ is a {\em proper subterm} of $N$ if $M$ is a subterm of $N$ and $M \not = N.$
We denote with $pst(\Gamma)$ the set of proper subterms of $\Gamma$,
and we define
$$
sst(\Gamma) = \{\sign M N \mid M, N \in pst(\Gamma) \}.
$$
The {\em saturated set} of $\Gamma$, written $St(\Gamma)$, is the set
$$
St(\Gamma) = \Gamma \cup pst(\Gamma) \cup sst(\Gamma).
$$
The cardinality of $St(\Gamma)$ is at most quadratic in the size of
$st(\Gamma)$. If $\Gamma$ is represented as a DAG, one can
compute the DAG representation of $St(\Gamma)$ in polynomial time, with only
a quadratic increase of the size of the graph.
Given a DAG representation of $St(\Gamma \cup \{M\})$,
we can represent a sequent $\Gamma \vdash M$ by associating
each node in the DAG with a tag which indicates
whether or not the term represented by the subgraph rooted at that node
appears in $\Gamma$ or $M$.
Therefore, in the following complexity results for deducibility problem
$\Gamma \Vdash_S M$ (for some proof system $S$), we assume that
the input consists of the DAG representation of the saturated set
$St(\Gamma \cup \{M\})$, together with approriate tags in the nodes.
Since each tag takes only a fixed amount of space (e.g., a two-bit data
structure should suffice), we shall state the complexity result
w.r.t. the size of $St(\Gamma \cup \{M\}).$

\begin{definition}
Let $\Gamma \Vdash_{{\cal D}} M$ be a deduction
problem, where ${\cal D}$ is some proof system, and let $n$ be the size of $St(\Gamma \cup \{M\}).$
Let $E$ be the equational theory associated with ${\cal D}$. Suppose that
the elementary deduction problem in $E$ has complexity $O(f(m)),$ where $m$ is
the size of the input.
Then the problem $\Gamma \Vdash_{{\cal D}} M$ is said to be {\em polynomially reducible}
to the elementary deduction problem $\Vdash_E$
if it has complexity $O(n^k \times f(n))$ for some constant $k.$
\end{definition}

A key lemma in proving the decidability result is
the following invariant property of linear proofs.
\begin{lemma}
\label{lm:St-inv}
Let $\Pi$ be an ${\cal L}$-derivation of $\Gamma \vdash M.$
Then for every sequent $\Gamma' \vdash M'$ occurring in $\Pi$,
we have
$\Gamma' \cup \{M'\} \subseteq St(\Gamma \cup \{M\}).$
\end{lemma}
The existence of linear size proofs then follows from the above
lemma.
\begin{lemma}
\label{lm:linear}
If there is an ${\cal L}$-derivation of $\Gamma \vdash M$ then there is an ${\cal L}$-derivation
of the same sequent whose length is at most $|St(\Gamma \cup \{M\})|.$
\end{lemma}

Another useful observation is that the left-rules of ${\cal L}$ are {\em invertible};
at any point in proof search, we do not lose provability by applying any
left rule. Polynomial reducibility of $\Vdash_{\cal L}$ to $\Vdash_E$ can
then be proved by a deterministic proof search strategy which systematically tries
all applicable rules.

\begin{theorem}
\label{thm:deducibility}
The decidability of the relation $\Vdash_{\cal L}$ is polynomially reducible
to the decidability of elementary deduction $\Vdash_E.$
\end{theorem}

Note that in the case where the theory $E$ is empty, we obtain a
\textsc{ptime} decision procedure for intruder deduction with blind
signatures.

\section{Some example theories}
\label{sec:examples}

We now consider several concrete AC convergent theories that are often used
in reasoning about security protocols. Decidability of intruder deduction
under these theories has been extensively studied
\cite{Comon-Lundh03LICS,Chevalier03LICS,Abadi06TCS,Delaune06ICALP,Lafourcade07IC,Cortier07LPAR}.
These results can be broadly categorized into those with explicit
pairing and encryption constructors, e.g., \cite{Comon-Lundh03LICS,Lafourcade07IC}, and those where the constructors
are part of the equational theories, e.g., \cite{Abadi06TCS,Cortier07LPAR}.
For the latter, one needs explicit decryption operators with, e.g., an equation like
$
dec(\enc M N, N) \approx M.
$
Decidability results for these deduction problems
are often obtained by separating elementary deducibility from
the general deduction problem. This is obtained by studying some form of normal
derivations in a natural deduction setting. Such a reduction, as has been shown
in the previous section, applies to our calculus in a more systematic fashion.

\paragraph{Exclusive-or.}
The signature of this theory consists
of a binary operator $\oplus$ and a constant $0.$ The theory is given by the axioms
of associativity and commutativity of $\oplus$ together with the axiom $x \oplus x \approx 0$
and $x \oplus 0 \approx x.$ This theory can be turned into an AC convergent rewrite system
with the following rewrite rules:
$$
x \oplus x \to 0 \qquad \hbox{ and } \qquad x \oplus 0 \to x.
$$
Checking $\Gamma \Vdash_E M$ can be done in PTIME, as shown in, e.g., \cite{Chevalier03LICS}.

\paragraph{Abelian groups.}

The exclusive-or theory is an instance of Abelian groups, where the inverse of
an element is the element itself. The more general case of Abelian groups includes
an inverse operator, denoted with $I$ here. The equality theory for Abelian groups is given by the axioms
of associativity and commutativity, plus the theory
$
\{ x \oplus 0 \approx 0, x \oplus I(x) \approx 0 \}.
$
The equality theory of Abelian groups can be turned into a rewrite system modulo AC by orienting
the above equalities from left to right, in addition to the following rewrite rules:
$$
I(x\oplus y) \to I(x) \oplus I(y) \qquad I(I(x)) \to x \qquad I(0) \to 0.
$$
One can also obtain an AC convergent rewrite system for an extension of Abelian groups
with a homomorphism axiom involving a unary operator $h$: $h(x \oplus y) = h(x) \oplus h(y).$
In this case, the rewrite rules above need to be extended with
$$
h(x \oplus y) \to h(x) \oplus h(y) \qquad h(0) \to 0 \qquad h(I(x)) \to I(h(x)).
$$
Decidability of elementary deduction under Abelian groups (with homomorphism)
can be reduced to solving a system of linear equations over some semirings
(see \cite{Delaune06IPL} for details).

\section{Combining disjoint convergent theories}
\label{sec:comb}

We now consider the intruder deduction problem under a convergent AC theory
$E$, which is obtained from the union of pairwise disjoint convergent
AC theories $E_1, \ldots, E_n.$ Each theory $E_i$ may contain an associative-commutative
binary operator, which we denote with $\oplus_i.$
We show that the intruder deduction problem
under $E$ can be reduced to the elementary deduction problem of each $E_i.$

Given a term $M = f(M_1,\ldots, M_k)$, where $f$ is a function symbol (i.e., a constructor,
an equational symbol or $\oplus$), the terms $M_1, \ldots, M_k$ are called the
{\em immediate subterms} of $M.$
Given a term $M$ and a subterm occurrence $N$ in $M$, we say that $N$ is a
{\em cross-theory subterm} of $M$ if $N$ is
headed with a symbol $f \in \Sigma_{E_i}$ and it is an immediate subterm
of a subterm in $M$ which is headed by a symbol $g \in \Sigma_{E_j}$, where $i \not = j.$
We shall also refer to $N$ as an {\em $E_{ij}$-subterm} of $M$ when we need to be explicit
about the equational theories involved.

Throughout this section, we consider a sequent system ${\cal D}$, whose rules
are those of ${\cal S}$, but with $id$ replaced by
the rule below left and
with the addition of the rule below right
where $N$ is a cross-theory subterm of some term in $\Gamma \cup \{M\}$:
$$
\infer[id_{E_i}]
{\Gamma \vdash M}
{
\begin{array}{c}
M \approx_{E} C[M_1,\ldots,M_k] \\
\hbox{$C[\ ]$ an $E_i$-context, and $M_1,\ldots,M_k \in \Gamma$}
\end{array}
}
\qquad
\infer[cs]
{\Gamma \vdash M}
{\Gamma \vdash N & \Gamma, N \vdash M}
$$

The analog of Proposition~\ref{prop:S-equal-N} holds for ${\cal D}$. Its proof is a straightforward
adaptation of the proof of Proposition~\ref{prop:S-equal-N}.

\begin{proposition}
\label{prop:D-equal-N}
The judgment $\Gamma \vdash M$ is provable in the natural deduction system ${\cal N}$, under theory $E$,
if and only if $\norm \Gamma \vdash \norm M$ is provable in the sequent system ${\cal D}$.
\end{proposition}

Cut elimination also holds for ${\cal D}$. Its proof is basically the same as the proof
for ${\cal S}$, since the ``logical structures'' (i.e., those concerning constructors)
are the same. The only difference is in the treatment of abstracted terms (the rules
$gs$ and $cs$). In ${\cal D}$ we allow abstraction of arbitrary cross-theory subterms,
in addition to guarded subterm abstraction.
The crucial part of the proof in this case relies on the variable abstraction
technique (Proposition~\ref{prop:var-abs} and Proposition~\ref{prop:var-abs2}),
which applies to both guarded subterm and cross-theory subterm
abstraction.

\begin{theorem}
\label{thm cut elim for D}
The cut rule is admissible for ${\cal D}$.
\end{theorem}

The decidability result for ${\cal S}$ also holds for ${\cal D}.$
This can be proved with straightforward modifications of the similar proof for ${\cal S}$,
since the extra rule $cs$ has the same structure as $gs$ in ${\cal S}.$
It is easy to see that the same normal forms for ${\cal S}$ also holds for ${\cal D},$ with $cs$
considered as a left-rule.
It then remains to design a linear proof system for ${\cal D}.$
We first define the notion of right-deducibility: The relation $\Gamma \Vdash_{{\cal R}{\cal D}} M$
holds if and only if the sequent $\Gamma \vdash M$ is derivable in ${\cal D}$ using only the right rules.
We next define a linear system for ${\cal D}$, called ${\cal L}{\cal D}$, which consists of
the rules of ${\cal L}$ defined in the previous section, but with the proviso $\Gamma \Vdash_{\cal R} M$
changed to $\Gamma \Vdash_{{\cal R}{\cal D}} M$, and with the additional rule:
$$
\infer[lcs]
{\Gamma \vdash M}
{\Gamma, R \vdash M}
$$
where $R$ is a cross-theory subterm of some term in $\Gamma \cup \{M\}$ and $\Gamma \Vdash_{{\cal R}{\cal D}} R.$

\begin{proposition}
A sequent $\Gamma \vdash M$ is provable in ${\cal D}$ if and only if it
is provable in ${\cal L}{\cal D}.$
\end{proposition}

The notion of polynomial reducibility is slightly changed.
Suppose each elementary deduction problem in $E_i$ is bounded by $O(f(m)).$
Let $m$ be the size of $St(\Gamma \cup \{M\}).$
Then the deduction problem $\Gamma \Vdash_{{\cal D}} M$ is polynomially reducible
to $\Vdash_{E_1}, \ldots, \Vdash_{E_n}$ if it has complexity
$O(m^k f(m))$, for some constant $k$.

\begin{theorem}
\label{thm:D-deducibility}
The decidability of the relation $\Vdash_{{\cal L}{\cal D}}$ is polynomially reducible
to the decidability of elementary deductions $\Vdash_{E_1},$ $\ldots,$ $\Vdash_{E_n}$.
\end{theorem}

\section{Conclusion and related work}
\label{sec:rel}

We have shown that decidability of the intruder deduction problem,
under a range of equational theories, can be reduced to the simpler
problem of elementary deduction, which amounts to solving equations in
the underlying equational theories. This reduction is obtained in a
purely proof theoretical way, using standard techniques such as cut
elimination and permutation of inference rules.

There are several existing works in the literature that deal with
intruder deduction.  Our work is more closely related to, e.g.,
\cite{Comon-Lundh03LICS,Delaune06IPL,Lafourcade07IC}, in that we do
not have explicit destructors (projection, decryption, unblinding),
than, say, \cite{Abadi06TCS,Cortier07LPAR}. In the latter work, these
destructors are considered part of the equational theory, so in this
sense our work slightly extends theirs to allow combinations of
explicit and implicit destructors.  A drawback for the approach with
explicit destructors is that one needs to consider these destructors
together with other algebraic properties in proving decidability,
although recent work in combining decidable theories
\cite{Arnaud07frocos} allows one to deal with them modularly.
Combination of intruder theories has been considered in
\cite{Chevalier05ICALP,Arnaud07frocos,DelauneIC08}, as part of their
solution to a more difficult problem of deducibility constraints
which assumes active intruders.  In particular, Delaune, et. al.,
\cite{DelauneIC08} obtain results similar to what we have here concerning
combination of AC theories.  One difference between these works and
ours is in how this combination is derived.  Their approach is more
algorithmic whereas our result is obtained through analysis of proof
systems.

It remains to be seen whether sequent calculus, and its associated
proof techniques, can prove useful for richer theories. For certain
deduction problems, i.e., those in which the constructors interact
with the equational theory, there does not seem to be general results
like the ones we obtain for theories with no interaction with the
constructors.  One natural problem where this interaction occurs is
the theory with homomorphic encryption, e.g., like the one considered
in \cite{Lafourcade07IC}. Another interesting challenge is to see how
sequent calculus can be used to study the more difficult problem of
solving intruder deduction constraints, e.g., like those studied in
\cite{Comon-Lundh03LICS,Chevalier03LICS,Delaune06ICALP}.

\paragraph{Acknowledgement}
We thank the anonymous referees of earlier drafts of this paper for
their careful reading and helpful comments. This work has been
supported by the Australian Research Council (ARC) Discovery Project
DP0880549.

redpajama_set_name: RedPajamaArXiv


text:
Hunters of cosmic ray particles come together in CREDO
Narwhal19 Posted on September 11, 2019
IMAGE: The CREDO Detector application transforms your smartphone into an important element of the largest particle detector in history. (Source: IFJ PAN) view more
A planet wide particle detector known as CREDO has been established by research and education organisations, bringing together individual citizen scientists from nearly every continent. All smartphone owners can participate in this undertaking that attempts to test the quantum structure of spacetime to the potential relationships between cosmic radiation and earthquakes and even the role played by high energy cosmic rays in cancer.
The international Cosmic-Ray Extremely Distributed Observatory (CREDO) project began in 2016 at the Institute of Nuclear Physics of the Polish Academy of Sciences (IFJ PAN) in Cracow, and is now transformed into a formal worldwide structure. Under the agreements signed, 25 institutional entities from 12 countries on 5 continents are currently involved in the construction of the global planetary particle detector CREDO: nine from Poland, three from the United States, two from Australia, the Czech Republic and Ukraine, and one each from Georgia, Mexico, Nepal, Russia, Slovakia, Uruguay and Hungary. They include scientific institutions that are significant not only on a Polish scale (including the Jagiellonian University, Cracow University of Technology, Astronomical Observatory of the University of Warsaw, IFJ PAN), but even globally (Massachusetts Institute of Technology). At the same time there is no shortage of educational entities, from the Copernicus Science Centre in Warsaw to primary schools. CREDO is made possible by a growing number of amateur enthusiasts, using their smartphones to register cosmic radiation particles.
"Expanding the boundaries of human cognition has always been, is and always will be a difficult process, with the increasing complexity and subtlety of the phenomena under investigation requiring ever greater financial, time and human resources," says Prof. Marek Jezabek, director of IFJ PAN. "That is why it is so important to skilfully use all the possibilities already present in existing equipment and to involve as many people as possible in the implementation of scientific projects – not only scientists but also enthusiasts. We are proud that the CREDO project, born in our Institute, is trying to implement these ideas both nationally and globally."
Project coordinator, Dr. Piotr Homola, professor at the IFJ PAN, explains its essence: "What makes the uniqueness of CREDO is the combination of data from very many different detectors recording particles associated with cosmic rays. We are talking here about fully professional detectors, built and managed by large centres or scientific consortia and often costing a lot of money, as well as those that are cheap, less sophisticated, but much more common, like CMOS sensors in the cameras of smartphones."
The CREDO project uses smartphones as detectors of cosmic radiation, known as cosmic rays. The camera in a smartphone detects a cosmic ray as a track across the CMOS when struck. As the camera are small, much less than a square centimetre in area, they are poorly suited for studying local phenomena like extensive air showers (i.e. cascades of secondary particles initiated by high-energy cosmic rays interacting with the Earth's atmosphere) reaching the surface of our planet. In the case of CREDO, the key is that smartphones are found in many places around the globe. Such large spread means that the collected data can track changes in time between the numbers of detected particles and learn about global changes in the cosmic ray numbers reaching the Earth.
One of the participants of the CREDO project aiming at detecting cosmic-ray ensembles is the Quantum Gravity Previewer experiment, searching for anomalies in the cosmic-ray arrival time distributions in single devices or local groups of detectors, mostly smartphones, in various places around the globe. The inspiration here is a scientific experiment from 1983, when in just five minutes, a network of cosmic ray detectors in Manitoba observed as many as 32 cases of extensive air showers (compared to just one that had been expected!). The study of such phenomena, currently incomprehensible to science, is one of the goals of CREDO and could explain, among others, whether the observed fluctuations result from the bizarre features of cosmic accelerators, or maybe from the effects of interactions of the products of particle decay with the quantum structure of spacetime.
Another research topic of the CREDO project is the impact of cosmic rays on human health. Although the average intensity of secondary cosmic radiation is not considered harmful (it is several times smaller than the intensity of the natural radioactivity of the environment), the impact on human health of extensive air showers, i.e. cascades of secondary particles initiated by cosmic rays with very high energies, has not yet been studied. The CREDO project will conduct this sort of pioneering research, going beyond the existing framework both in the fields of the physics of cosmic radiation itself and knowledge about the possible biological response of the human body to this radiation. These studies will be conducted taking into account global trends in understanding the impact of low doses of radiation on living organisms in terms of the possibility of the occurrence of both positive phenomena (e.g. increasing the immunity of organisms) and negative ones (e.g. diseases of unknown aetiology, including some types of cancer).
CREDO has the chance to verify another spectacular hypothesis, so far measured only once – concerning the relationships between earthquakes and changes in the cosmic ray flux reaching the surface of our planet. It is assumed that stresses in the Earth's crust can generate anomalous electromagnetic fields above the surface, which would affect the number of cosmic ray particles registered. If the phenomenon were confirmed, quantitatively examined and understood, we might even be tempted to design warning systems against impending earthquakes.
To connect your smartphone to the CREDO detector cloud, simply install the CREDO Detector app from your smartphone's store, and run it with the camera lens covered (see https://credo.science/ for details). The maintenance and development of this app is supervised by the Cracow University of Technology, and the Academic Computer Centre CYFRONET of the AGH University of Science and Technology in Cracow supervises the collection and processing of data from around the world (not only from smartphones).
CREDO is a doubly open observatory. Anyone can join with their data, anyone can also access all the scientific data (with, of course, full respect for the privacy of users). This also applies to the implementation of scientific ventures which have not yet been included in the formal research programme of the project.
The initiators of CREDO strive to appreciate all the entities involved in the project, including people from outside the formal world of science. Co-founders of CREDO have the right to co-authorship of scientific publications based on the collected data. In turn, you can keep track of the graphs created in current experiments on the project website. All users can check the input of their data here, and can also become involved in all the analyses.
"We believe that scientific projects should enable not only data collection, education or individual development, but should also give perhaps not fully scientific but still very satisfying cognitive pleasure", emphasizes Prof. Homola. "In this spirit, we've thought up the continuous Particle Hunters contest, aimed mainly at pupils and students, enabling individual and team competition between smartphone owners. Currently, over 1,200 pupils from around 60 schools are participating in the competition. For now, these are Polish schools, but we hope that over time, the competition will expand to other countries."
Smartphones are just one type of detector recording cosmic ray particles within CREDO. Soon, networks of small and inexpensive detectors like Cosmic Watch will be able to transmit their data. Networks of this type can be constructed even by not very advanced electronic amateurs, modelling, for example, on an open project originally developed by MIT for the famous IceCube neutrino detector.
The openness of CREDO enables the practical and immediate inclusion of professionals in the project, allowing them to analyse data that for others are just an unnecessary or even unwanted background. These include muons of cosmic origin, recorded by professional ultra-high energy cosmic ray observatories, neutrino and dark matter detectors, astronomical observatories equipped with telescopes with CMOS sensors, as well as accelerator centres with their specialist elementary particle detectors.
"The real strength of CREDO lies in its physical multiculturalism. We try to combine data on different types of radiation, with different energies, recorded by different methods. We hope that in this way we will open a new window to the Universe and better understand the fundamental features of our reality," sums up Prof. Homola.
More information on cosmic radiation and the CREDO project can be found in the press package associated with this press release. The package is available in the IFJ PAN press service at: https://press.ifj.edu.pl/.
The Henryk Niewodniczanski Institute of Nuclear Physics (IFJ PAN) is currently the largest research institute of the Polish Academy of Sciences. The broad range of studies and activities of IFJ PAN includes basic and applied research, ranging from particle physics and astrophysics, through hadron physics, high-, medium-, and low-energy nuclear physics, condensed matter physics (including materials engineering), to various applications of methods of nuclear physics in interdisciplinary research, covering medical physics, dosimetry, radiation and environmental biology, environmental protection, and other related disciplines. The average yearly yield of the IFJ PAN encompasses more than 600 scientific papers in the Journal Citation Reports published by the Thomson Reuters. The part of the Institute is the Cyclotron Centre Bronowice (CCB) which is an infrastructure, unique in Central Europe, to serve as a clinical and research centre in the area of medical and nuclear physics. IFJ PAN is a member of the Marian Smoluchowski Kraków Research Consortium: "Matter-Energy-Future" which possesses the status of a Leading National Research Centre (KNOW) in physics for the years 2012-2017. The Institute is of A+ Category (leading level in Poland) in the field of sciences and engineering.
Dr. Piotr Homola, professor at the IFJ PAN
The Institute of Nuclear Physics, Polish Academy of Sciences
email: piotr.homola@ifj.edu.pl
https://credo.science/
The website of the Cosmic-Ray Extremely Distributed Observatory (CREDO).
http://www.ifj.edu.pl/
The website of the Institute of Nuclear Physics Polish Academy of Sciences.
http://press.ifj.edu.pl/
Press releases of the Institute of Nuclear Physics Polish Academy of Sciences.
IFJ190911b_fot01s.jpg
HR: http://press.ifj.edu.pl/news/2019/09/11/IFJ190911b_fot01.jpg
Prof. Marek Jezabek, director of the Institute of Nuclear Physics of the Polish Academy of Sciences in Cracow, signs an agreement on formal accession of the Institute to the international CREDO project. (Source: IFJ PAN)
The CREDO Detector application transforms your smartphone into an important element of the largest particle detector in history. (Source: IFJ PAN)
Tagged:airatmosphereAustraliaBiologycamerascompetitionConstructionContestCzech RepublicDataDesigndistributedEarthEducationEnergyEngineeringEnvironmentEnvironmentalEuropeexpandinggeorgiaglobalHealthHistoryInfrastructureInternationalKnowledgeKrakówLivingMassachusettsMassachusetts Institute of TechnologyMedicalmexicominutesMITMoneynationalNaturalNepalNuclearOROtherOur PlanetoutsidePeoplephysicsPolandPositivePrimary schoolsPrivacyquantumResearchResourcesRussiaSchoolsScienceScience and TechnologyshowersSlovakiasmallstatesStudentsTechnologytimeUkraineUnited StateswarsawWorld
Previous PostSquirrels Savagely Stealing Acorns | Spy In The Wild | BBC Earth
Next PostSee What's Under The "Frunk" Of A Tesla Model 3
'Doomism' or Reality? Divided Over Its Message, the Climate Movement Seeks Balance – InsideClimate News
ADAPTATION: Escape plan for rising seas: Floating cities (or a barge)
Narwhal19 December 23, 2020
New Jersey Joins Other States in Suing Fossil Fuel Industry, Claiming Links to Climate Change – InsideClimate News
Melting small glaciers could add 10 inches to sea levels
Narwhal19 May 23, 2019

redpajama_set_name: RedPajamaCommonCrawl


text:
Angie D. Devanney, Mayor
Current term expires:
adevanney@bhtwp.com
As your new Mayor, I am excited to be working with all residents to write the next chapter of our town's history. That new chapter began on January 1, where I was ceremonially sworn in as Mayor by a large group of Berkeley Heights girls who had helped to help elect me. As the first woman to be elected Mayor by the voters, it was an historic moment that I was proud to be part of!
My first few months have been very busy, and I am pleased to report that progress has already been made on several fronts. Township officials who bring excellent experience and capabilities were appointed. I made many appointments to Township committees following an unprecedentedly open and transparent application process. They are of different political views and supported different candidates for office, and all are highly capable and qualified. First and foremost was their commitment to making Berkeley Heights a better place to live. In other words, they fulfill the "purple" vision of our Township that I was elected to bring about.
In my Inaugural Address, I spoke of the need to manage our tax dollars better. To that end, the Township has adopted contracts for services under a new, professional standard known as a Request for Qualifications (RFQ), which also conforms to the state standard of Fair and Open contracts. This measure will help keep costs down while making the process much more transparent. Other, equally responsible measures have and will be implemented in the weeks and months ahead.
Our new Recycling Taskforce which will explore options to bring down costs of our increased recycling budget. Additionally, working with Council, I would like to create an Economic Development committee designed to bolster our local business. We hope the committee will explore and launch "SHOP BH," a property tax discount program that discounts your taxes when shopping at a local participating business. Meanwhile, our Department of Public Works and Engineering Departments are hard at work putting together a comprehensive drainage, sewer and road repair schedule to address long overdue infrastructure challenges.
And, I am committing to doing everything I can to increase a sense of connectedness between our residents and our local government. Through effectively utilizing social media, to regular "Mayor's Corner" columns in TAP, to video and community outreach efforts, this administration is placing a heavy emphasis on making sure residents feel heard, and that their input is valued.
Mayor Angie Devanney was sworn in as Berkeley Heights' first elected female Mayor on January 1, 2019.
She previously served as Berkeley Heights Township Administrator from 2004-2007, and was was named Business Administrator of the Year in 2004 by the Regional Gateway Chamber of Commerce. In 2005, she was awarded the Women of Excellence Award in the area of Environmental Advocacy. She recently retired from serving as the Mountain Park PTO President, is currently the Secretary to the Berkeley Heights Police Athletic League (BH PAL), and a small business owner.
Angie gained vast knowledge of town operations and experience during her time as Township Administrator; she ran business operations, overseeing the departments of DPW Public Works, Engineering, Finance, Zoning/Construction and Public Safety. She is skilled at creating shared services; such as the agreement she reached with the County in IT and printing. Her experience and relationships in local, county and state government will allow Berkeley Heights to maximize grants funds and other resources.
Angie is married to George Devanney and has two children: Ryan, a junior at Governor Livingston High School, and Abbey, a 5th grader at Mountain Park Elementary.
You can email Mayor Devanney at adevanney@bhtwp.com
Apply to Become a Committee Member
Submit an application to become a Township volunteer.
The Township welcomes and encourages residents who have specific experience applicable to each Committee, Board and Commission to apply for available positions. Please note that there are only a few volunteer opportunities available each year as there are staggered terms for members of each Committee, Board and Commission. However, many committees are always in need of extra volunteers for various events throughout the year.
The Township of Berkeley Heights is governed by the Mayor /Council /Administrator form of local government.
Term Overview
As a variant of the Faulkner Act, the Mayor is directly elected by the voters and serves a term of four years. Council members are elected to serve three year terms. Council terms are staggered so that two Council seats are up for election each year.
Voters Elect
The voters elect section is comprised of the Mayor and 6 council members:
Council: Staggered 3 year term
Mayor: 4 year term
Organization of Governing Body
The governing body is organized on January 1.
The Mayor:
Appoints:
Department heads with Council approval
Municipal clerk
Has veto subject to override by 2/3 of all Council members
May remove department heads upon written notice to Council
Presides over Council and Exercises the executive power of municipality
Votes only to break ties
Approves Mayor's appointees for:
Department heads
Exercises legislative power of the municipality
May remove department heads for cause after a hearing
Prepares budget with assistance of municipal administrator and treasurer
Mayor exercises executive power of the municipality. Up to six departments may be created by ordinance. Administrator supervises administration of each department.
Angie D. Devanney


We have studied that Reality or Sachchidananda is a triune of Existence-Consciousness-Bliss, We have also mentioned that these are not additive terms but different poises of the same Reality.
In Chapter X of the Life Divine, Sri Aurobindo modifies the nature of Sachchidananda by introducing the dimension of Force (or Shakti or Tapas) as an integral aspect of the Absolute Consciousness. Consciousness (Chit) is not merely consciousness or awareness but a 'complex' of 'Consciousness-Force' or 'Chit-Shakti'. 'Force' is as inseparable from consciousness as is the power of fire from fire. Sri Aurobindo explains that the manifestation of consciousness through creation is possible because of the presence of the Force or Shakti, otherwise the Absolute Consciousness (which mystics perceive as 'pure' consciousness or Chit) would have remained in its poise of indivisibility and immobility.
This chapter also provides a definition of consciousness that would be equally relevant to the different types of consciousness researchers—psychologists, physicists, mathematicians, and metaphysicians.
At the scientific level, there are two major approaches in consciousness research. The first approach starts from neurophysiology and extends to psychology. The second approach starts from the physicist's level of matter-energy and uses different models to understand both the physical and non-physical qualia of consciousness. Both the approaches have helped to throw some light on how consciousness acts but both have failed to reveal the true nature of consciousness.
The limitations of these approaches were previsioned in the second decade of the last century when Sri Aurobindo wrote that our ordinary understanding of a 'mental waking consciousness' when one is 'not asleep, stunned or otherwise deprived of his physical and superficial methods of sensation' (The Life Divine, pg 94) was too limited to be generalized and too simplified to be relevant.
Actually, data from research of these three dimensions have resulted in such intriguing observations that our hypotheses of consciousness need constant reconstructions. Sleep cannot be today considered as 'unconscious' .In fact, sleep is now considered to be an active physiological process and not a mere failure of arousal and is clearly separable from stupor (a situation where a subject can only be 'aroused' by vigorous and continuous external stimulation) and coma (a situation where a subject elicits no response to any external stimulus or inner biological need). As sleep is not a failure of arousal, it is not surprising that we experience a rich and variegated dream-life that reveals the personal and collective unconscious. Dreams also at times carry future premonitions though we are not sure how they occur. In contrast to sleep, stupor and coma are states where the 'arousal' mechanism seems to fail and may ultimately lead to death. Yet, stupor and coma may not be as dry and colourless as they externally appear. The reporting of large number of NDE (Near Death Experiences) cases raises many interesting issues. Due to advanced resuscitation techniques available today, it is possible to bring back to life subjects who where at the verge of death or 'technically dead' for a few moments. A commonality in the reported experiences of these subjects is emerging which usually include having a life-review, traversing a tunnel, encountering a Being of Light, and rarely getting premonitions of the future. What is more important for psychiatry is that these subjects are often reported to have lasting personality changes after being resuscitated. Besides, one may also infer that folklore concepts of 'Judgment Day' and 'angels' may have arisen from suprasensorial experiences similar to experiences of NDE subjects. A purely mechanistic view-point would dismiss the NDE as a mere organic happening (a temporal lobe phenomenon or something allied or a hallucination) but that does not rule out the interesting fact that a subject in stupor or coma whose 'arousal' mechanism is inhibited is still capable of a colourful inner experience that can even result in personality changes once the arousal mechanism is facilitated again. If the NDE is considered something akin to a dream, then also we are left intrigued. If dreams or allied phenomena occur both during sleep (where there is no failure of 'arousal') and during coma (where there is a failure of 'arousal'), then how do we explain the origin of dreams? Do dreams arise from a pre-existing world of dreams that uses the brain as an instrument for expression (just as many mathematicians believe that there is a pre-existing world of numbers which they go on discovering)? Indeed, the whole spectrum of 'NDE' experience suggests that in between 'coma' and 'death', a portion of the individual's consciousness gets dissociated and traverses ranges of the universal consciousness of which we are not ordinarily aware. The NDE phenomenon raises another question: can a non-material principle of one's being traverse subtle ranges of consciousness even after brain death? At present our scientific knowledge is too limited to even speculate on this proposition. Yet, it is interesting to note that subjects undergoing anesthesia often report 'Out of Body Experiences' (OBE) where a portion of their consciousness seems to get dissociated so that they can report 'visualizing' surgical operations being conducted on their own bodies or events that occur at a distance.
Another interesting area of consciousness research is the zone of altered states of consciousness. This is not a homogenous zone but seems to reveal that mystical experience can be indicative of a different type of consciousness. Thus, experiments have shown that subjects practicing meditation (like Raj yoga) have certain EEG changes (usually an increase of slow –alpha waves in the frontal and central regions of the brain) along with reduced metabolism. Such physiological changes are not seen in trance states induced through hypnosis, ritualistic dancing and revivalist meetings. Physiological changes during meditation have distinctive characteristics which are different from the neurovascular changes (probably endorphin mediated) accompanying rituals like instances where subjects neither feel pain nor bleed even when they inflict harm on themselves (piercing one's own tongue or cheek, walking unscathed through fire, lying on a bed of thorns or allied phenomena seen in different cultures).Recently it has been demonstrated that after a month of regular meditative practices, there is an increase in myelination (the protective fatty insulation surrounding nerve fibres) as well as increase in axon density (signifying greater number of brain signaling connections) in the anterior cingulated cortex of the brain that regulates behaviour. This finding could suggest new healing pathways for several mental disorders.
So long, we were focusing on the 'states' of consciousness modulated through the ascending reticular system that can be in a state of 'arousal' or 'inarousal'. Neurophysiology also studies the 'contents' of consciousness like sensations, emotions, images, memories, and ideas. The content of consciousness depends upon structures in the brain, lesions of which can diminish the content while the state of consciousness may or may not be changed. Thus, in the case of a brain tumour, there might be an emotional change (a change in 'content') and the subject may later lapse into coma ( a change in 'state').In a case of dementia, there might be a diminution of the 'content' of consciousness with shrinking of memory and emotional blunting while the 'state' of consciousness or arousal remains normal. It is very surprising that even after total bilateral destruction of the cerebral hemispheres, sleeping and waking can still occur in some subjects.
The scientists who use the matter-energy approach to understand consciousness also work through different models - physical, biological, quantum, information processing, computational and other allied models.
It is claimed that all these approaches have understood the basic workings of consciousness except one area-how can consciousness with its 'richness' and 'variety' emerge from matter that is inert, inconscient, colourless and dull?
Sri Aurobindo points out that one cannot explain the appearance of consciousness out of inanimate matter unless one accepts a Being behind who applies the force and also becomes matter. (Sri Aurobindo, Evening Talks, January 8th, 1940, pg. 701) It is this being who has been experientially perceived as Sachchidananda—a 'Pure Existent' who is also Chit or 'Pure Consciousness'.
The problem is how we relate Chit or pure consciousness to the diverse phenomena that science groups under the umbrella of 'consciousness studies'.
Science studies 'consciousness' in terms of 'matter-energy' or as neurophysiological processes. When spirituality studies consciousness, it uses an intuitive, experiential approach resulting in an absolutist, subjective realization that is not dependent on any objective validation. It is in this way that the spiritual paradigm perceived consciousness as Chit or the 'pure' essence of Reality.
Thus, spirituality deals with the essence of Reality or Chit that is beyond manifestation. Science deals with the phenomena of consciousness in existence, within the manifestation. As science and spirituality are dealing with two different paradigms of Reality, is there any necessity to integrate them?
The problem arises because both science and spirituality use the same term 'consciousness' to describe their versions of Reality. It might have been simpler if they had used different terms!
The problem persists because Sri Aurobindo is an Integralist. It is his mission to integrate science and spirituality. He is not bothered about the apparent irreconcilability of science and spirituality for He views all problems of existence as problems of harmony.
(b) The phenomena of consciousness that works through matter-energy—phenomena that science studies and which spirituality groups under 'Nature' or 'Prakriti'.
Sri Aurobindo solves this problem by incorporating 'Energy' or 'Force' in the very substance of Chit—by placing 'Force' as an in-built mechanism within the matrix of Chit. Thus Chit is not merely chit but Chit-Shakti or Conscious-Force.
Sri Aurobindo describes 'CHIT' to be 'the universal conscious stuff of existence' that is manifested in many poises. There is the poise of the mental self-awareness in human beings where the pure action of Chit gets limited; there is the poise of a still limited consciousness in terrestrial forms below the level of human beings in the scale of evolution while at the level of matter, Chit gets so limited that it appears to be inconscient. There are also higher poises (experienced by Yogis and mystics) where Chit can manifest with greater potentialities than in ordinary mentality.
The manifestation of 'Chit' automatically implies that there is an 'energy' or 'force' at work.
Thus, in the Aurobindonian perspective, consciousness is simultaneously the self-awareness inherent in existence and the conscious-force that builds the universe. Awareness by itself is not enough as there must be a will or 'Force' or 'Executive Energy' that makes the consciousness effective.
As Conscious Force, consciousness is impregnated with and expressive of purpose and meaning at all levels. Thus it is nuclear energy at the level of matter, life in plants, instinct in insects and animals, mental intelligence, will and feeling in human beings, and powers higher than the mind (viz. intuition, revelation) in mystics and yogis.
The concept of Chit-Shakti that signifies a movement towards creation initiated in the bosom of an immobile Consciousness brings another dilemna, which Sri Aurobindo has to solve too. Spiritual experience has perceived an ABSOLUTE EXISTENCE BEYOND ALL MANIFESTATION WHICH IS NOT COMPELLED TO MOVE. HOW DOES THIS MOVEMENT ALIEN TO THE ETERNAL REPOSE OF CONSCIOUSNESS COME TO TAKE PLACE IN IT?
II.2.8. This that wakes in the sleepers creating desire upon desire, this Purusha, Him they call the Bright One, Him Brahman, Him Immortality, and in Him are all the worlds established: none goes beyond Him.
This is That thou sleekest.
II.2.13.The One Eternal in the transient, the One consciousness in many conscious beings, who being One orders the desires of many: the calm and strong who behold Him in their self as in a mirror, theirs is eternal peace and 'tis not for others.


text:
The Narcissistic Life takes your privacy seriously. This privacy policy describes what personal information we collect and how we use it. See this privacy policy primer to learn more about privacy policies in general.
Routine Information Collection
All web servers track basic information about their visitors. This information includes, but is not limited to, IP addresses, browser details, timestamps and referring pages. None of this information can personally identify specific visitors to this site. The information is tracked for routine administration and maintenance purposes.
Where necessary, The Narcissistic Life uses cookies to store information about a visitor's preferences and history in order to better serve the visitor and/or present the visitor with customized content.
Advertising partners and other third parties may also use cookies, scripts and/or web beacons to track visitors to our site in order to display advertisements and other useful information. Such tracking is done directly by the third parties through their own servers and is subject to their own privacy policies.
Controlling Your Privacy
Note that you can change your browser settings to disable cookies if you have privacy concerns. Disabling cookies for all sites is not recommended as it may interfere with your use of some sites. The best option is to disable or enable cookies on a per-site basis. Consult your browser documentation for instructions on how to block cookies and other tracking mechanisms. This list of web browser privacy management links may also be useful.
Mediavine Programmatic Advertising (Ver 1.1)
The Website works with Mediavine to manage third-party interest-based advertising appearing on the Website. Mediavine serves content and advertisements when you visit the Website, which may use first and third-party cookies. A cookie is a small text file which is sent to your computer or mobile device (referred to in this policy as a "device") by the web server so that a website can remember some information about your browsing activity on the Website.
First party cookies are created by the website that you are visiting. A third-party cookie is frequently used in behavioral advertising and analytics and is created by a domain other than the website you are visiting.
Third-party cookies, tags, pixels, beacons and other similar technologies (collectively, "Tags") may be placed on the Website to monitor interaction with advertising content and to target and optimize advertising. Each internet browser has functionality so that you can block both first and third-party cookies and clear your browser's cache.
The "help" feature of the menu bar on most browsers will tell you how to stop accepting new cookies, how to receive notification of new cookies, how to disable existing cookies and how to clear your browser's cache. For more information about cookies and how to disable them, you can consult the information at All About Cookies.
Without cookies you may not be able to take full advantage of the Website content and features. Please note that rejecting cookies does not mean that you will no longer see ads when you visit our Site. In the event you opt-out, you will still see non-personalized advertisements on the Website.
The Website collects the following data using a cookie when serving personalized ads:
Operating System type
Operating System version
Language of the website
Web browser type
Email (in hashed form)
Mediavine Partners (companies listed below with whom Mediavine shares data) may also use this data to link to other end user information the partner has independently collected to deliver targeted advertisements.
Mediavine Partners may also separately collect data about end users from other sources, such as advertising IDs or pixels, and link that data to data collected from Mediavine publishers in order to provide interest-based advertising across your online experience, including devices, browsers and apps.
This data includes usage data, cookie information, device information, information about interactions between users and advertisements and websites, geolocation data, traffic data, and information about a visitor's referral source to a particular website. Mediavine Partners may also create unique IDs to create audience segments, which are used to provide targeted advertising.
If you would like more information about this practice and to know your choices to opt-in or opt-out of this data collection, please visit National Advertising Initiative opt out page. You may also visit Digital Advertising Alliance website and Network Advertising Initiative website to learn more information about interest-based advertising. You may download the AppChoices app at Digital Advertising Alliance's AppChoices app to opt out in connection with mobile apps, or use the platform controls on your mobile device to opt out.
For specific information about Mediavine Partners, the data each collects and their data collection and privacy policies, please visit Mediavine Partners.
Special Note About Google Advertising
Any advertisements served by Google, Inc., and affiliated companies may be controlled using cookies. These cookies allow Google to display ads based on your visits to this site and other sites that use Google advertising services. Learn how to opt-out of Google's cookie usage. As mentioned above, any tracking done by Google through cookies and other mechanisms is subject to Google's own privacy policies.
Concerns or questions about this privacy policy can be directed to amburgemeester@gmail.com for further clarification.
This privacy policy was generated by the Privacy Policy for WordPress plugin.


Welcome to March's edition of Cooking Jamboree with Brig and Ian, Cooking Jamboree 2: Electric Boogaloo. We will be making a fancy multi-cheese Italian pizza and an gooey batch of fudge brownies.
Next give the dough a nice spreading. Toss that bad boy in the air like you just don't care and give it a spin on the ole tactile member. Once the dough is spread to your satisfaction, place it on the greasy pan and prepare to sauce that baby up.
Crack open a can of your favorite sauce, and put a layer of it on the dough while avoiding the crust. Be sure you have an even layer of sauce on the pizza or you may get a pizza that's way too saucy.
Bust open your bag of cheese, cover the pizza in a layer of the cheese of your choosing. Proportion the amount of cheese to balance out the sauce, you will thank us later. If you are a flavor connoisseur like us, feel free to add any cheeses to enhance the flavor profile of your creation.
Once the pizza has been cheesed to your heart's desire, throw that baby in the oven for a nice even eighteen minutes, or until it is golden on the crust and fully cooked.
Grab your favorite cutting utensil and cut yourself a nice steamy hot slice dripping with fancy cheese and hopefully some mozzarella slices.
First preheat the oven to 350, then grab a bowl for mixing/pouring and a pan to cook the brownies in, we used a medium sized glass one. Once you've got them, get the pan nice and greasy with some sort of butter.
Next you gotta whip up the batter. Put two eggs in the bowl, half a cup of vegetable oil, three tablespoons of water, and the box of brownie mix. We used a power mixer for maximum blending speed, but a hand mixer or spoon will work just as well.
Once the mixture seems to be a brown creamy liquid of goodness, gracefully pour it into your pre buttered pan in a nice even layer.
Put it in the oven for around eighteen minutes. At eighteen minutes you need to check and see if they are done. Take a toothpick and stick it into the top of the brownies to the bottom of the pan, and remove it. If it comes out easily and there is no liquid brownie on the bottom, your brownies are done. If they aren't then leave them in and wait a few minutes then check again.
Let them cool for a bit so you can cut the brownies evenly. If you please, you can also add frosting, sprinkles, or even more butter to the top layer. Lastly, enjoy your brownies.


Mary Jane Walker is pleased to announce the launch of the fifth in her series of unconventional accounts of world travel, A Maverick USA Way.
A Maverick USA Way is the United States as seen and experienced from the Antipodean point of view by Mary Jane, a regular visitor to the USA since 1996.
On her latest trip, Mary Jane took advantage of direct flights between Auckland and Houston to arrive in the American heartland, a change from Los Angeles.
She visited the Space Museum and learned how the Apollo program might have led to solar power from space, but didn't.
Mary Jane rode the Amtrak tracks around the lower 48 states and passed through the Dakotas twice, the second time to catch up with the anti-Keystone pipeline protests at Standing Rock.
A protestor asked to use her phone at the Bismarck public library and she gave him a lift, so she got straight into the heart of the camp.
She hired 14 cars and listened to a musician on the train, who said that Johnny Cash was more authentic than Elvis because he wrote all his owns stuff.
Hiking in Glacier, Yellowstone, Yosemite and Rocky Mountain National Parks proved quite different to New Zealand. People needed bear-proof containers, electric fences and bear spray. Another hiker told her how his father had hoisted him onto his shoulders to keep from being eaten by a hungry mountain lion.
Detroit was a stately Art Deco city reverting to parkland, like ancient Rome after its fall.
Mary Jane was in the USA for the elections and saw a lot of discontent; she was not surprised Trump won.
On the way home she stopped off in Hawaiʻi and took in the view of the volcanoes, while noticing how many homeless people seemed to gravitate to the islands.
For any further information, please contact Mary Jane or her editor Chris Harris by email to admin [at] a-maverick.com.


Fastnbulbous They exude similar darkwave energy as bands like Beastmilk, but not as heavy, with guitars that ring and chime rather than slash. Think early Comsat Angels with Johnny Marr's melodicism, coloring their Ian Curtis influence with Lawrence's (Felt) vocal mannerisms. - fastnbulbous.com/early-2015-postpunk-rundown/ Favorite track: Dispersed Energy.
Peefogg Voilà typiquement le genre de track qui fait basculer un album dans la catégorie supérieure !
Excellent ! Favorite track: Old.
Includes unlimited streaming of Poverty via the free Bandcamp app, plus high-quality download in MP3, FLAC and more.


State Rep. Terri Bryant (R-Murphysboro) received the Governor's signature on her first piece of legislation on Tuesday. Back in April, Bryant received unanimous support in the House for HB 3721, a bill designed to help National Guard members keep their jobs. Bryant, whose district shares a border with the state of Missouri, explained the need for the measure.
"When a member of the National Guard is called to duty by their own state's Governor or by the Governor of a neighboring state, this bill would allow them to categorize their work as military service," Bryant said. "The addition of a 'military service' definition to their work in another state affords members of the National Guard protection that their job will be held for them upon a call up to duty in another state."
Bryant said that while the change may seem small, it is quite significant for the men and women of Illinois serving in the National Guard. Read more.


text:
Trump White House
White House Defends Trump's Bizarre Tweet About "Bidan" and North Korea
The president again downplayed North Korean missile launches, and tried to bond with Kim Jong-un over jabs at Joe Biden.
By Kevin Fitzpatrick
Kimimasa Mayama/Getty Images.
Pay no attention to the authoritarian camaraderie behind the psychotic tweets, press secretary Sarah Sanders reiterated on cable news for the thousandth time on Sunday. This time around, the beleaguered secretary was defending another of President Trump's bizarrely cozy missives about North Korea—in which he suggested that Kim Jong Un might be winking at him when the dictator made a "low IQ" reference to 2020 rival Joe Biden.
"North Korea fired off some small weapons, which disturbed some of my people, and others, but not me," Trump tweeted during a trip to Japan. "I have confidence that Chairman Kim will keep his promise to me, & also smiled when he called Swampman Joe Biden a low IQ individual, & worse. Perhaps that's sending me a signal?" Trump initially had to delete the tweet, having misspelled the name of his rival as "Bidan."
By Sunday, Sanders was telling Chuck Todd of NBC's Meet The Press not to worry about the U.S. president voicing affection for a murderous dictator over a former vice president. "The president's not 'siding' with that," Sanders stated of the tweet. "But I think they agree in their assessment of former Vice President Joe Biden. . . . The president doesn't need somebody else to give him an assessment of Joe Biden. He's given his own assessment a number of times. The president watched him and his administration with President Obama fail for eight years. He's come in in two and a half, he's cleaned up a lot of the messes that were left behind."
Trump was referring to a statement by North Korean state media earlier in the week, which labeled Biden a "fool of low IQ" and "an imbecile bereft of elementary quality as a human being, let alone a politician." Following Trump's tweet, a Biden spokesperson told ABC News, "Given Vice President Biden's record of standing up for American values and interests, it's no surprise that North Korea would prefer that Donald Trump remain in the White House."
The casual tweet also did not appear to rattle Japanese Prime Minister Shinzo Abe, even as the country is within range of—and frequently saber-rattled by—North Korean missiles. Trump has otherwise discussed the possibility of holding yet a third summit with Kim Jong-un, while Abe himself has reportedly entertained the possibility of his own meeting with the North Korean leader.
Get the Hive Newsletter
The freshest-and most essential-updates from Washington, Wall Street, and Silicon Valley.


As of today, women in Saudi Arabia are allowed to drive. King Salman, by royal decree declared that drivers licence can now be issued to women.
This runs counter to the countries long history of patriarchal conservatism that has traditionally limited women's freedoms.
Dr Ben Rich of Curtin University spoke to Chris Butler on The Mag.


text:
Happy 35th Birthday EPCOT: Our Favorite Memories
Posted on October 1, 2017 by Sophie Brown • 0 Comments
Spaceship Earth at EPCOT, Image: Sophie Brown
As EPCOT (or EPCOT Center, as it used to be known) reaches its 35th birthday today, the GeekMoms have been reminiscing about our favorite memories of one of the world's most unique theme parks and the things we love about it. Below, some of us share our thoughts about what makes this place so special to each of us.
Sombrero Photos Taken Ten Years Apart (2004 and 2014), Images: Sophie Brown
I first visited EPCOT in 2004 during my very first trip to Walt Disney World, and it instantly became my favorite of the four Disney Parks–well, maybe joint first with the Magic Kingdom. During that trip, I was inducted into a special club. No, not Club 33, unfortunately, but the Sombrero Club. You see, ever since my husband's family started visiting Disney World, they had taken a photo of their vacation group in EPCOT's Mexico pavilion, each wearing a sombrero. These photos stretched back to 1988 and, over the years, had become a timeline of change. Different people joined the groups and left. Children grew and became adults. In the very first Sombrero Club photograph, my husband was only 14 years old. The most recent one shows him stood beside our son, then aged five. There are Sombrero Club photos of my nieces and nephews, one taken on my honeymoon, ones including friends who came with us one particular year. What started out as a fun family picture has grown into something we can look at and see the changes in our family, even as the scene behind us remains almost identical through the years. It's something that has become a must-do on every trip into EPCOT, and something I hope will be passed down to future generations.
The Japan Pavilion, Image: Sophie Brown
Jenny Bristol
Our first time at Disney World, it was the early '80s. There was only The Magic Kingdom, but my sister remembers that they were building E.P.C.O.T. (with the periods) at the time. Fast forward to 2006 and, now with two kids in tow, we finally made it back to the Disney World resort. By this time, there were four main parks, plus sprawling resort hotels and the like. I had planned on eight days in the parks, most of which we spent in The Magic Kingdom and EPCOT (now without periods). Though I craved moving walkways, since it was Florida in August, EPCOT pretty much embodied much of my personality. Its two halves, one focusing on science and the future and the other one on travel and culture, combined to create a strange whole that just made me happy. We jumped from science thing to science thing, and then did the whole round of the World Showcase. I especially loved how they took great care to design the country areas authentically, with the Best Food Ever (TM) and shops that made you feel like you were actually in the country. I may have gone a little wild in the Japanese store. I am dying to go back with Rory and the kids so we can experience it all together, with the kids actually remembering stuff this time, since they were five and two when we went. But this time, it won't be in August.
A Marching Band at Disney World, Image: Disney
Patricia Vollmer
My first trip was in summer 1988 (like Sophie's husband's family's first sombrero photo!) I was a strolling violinist in a group through my school system and someone had donated a LOT of money for our group to perform through the Magic Music Days program. While most of what visitors see with Magic Music Days are on the order of marching bands down Main Street and choral performances, ours was unique in that we were put in the Odyssey Restaurant in EPCOT to stroll through a lunch seating. For our group, well, this was what we did, so it wasn't too difficult, but it was definitely magical to do it at Disney World! One of the things I remembered about this experience was getting to use one of the cast dressing rooms that apparently was also used for the Disney characters because there were posters with tips on how Mickey and Minnie Mouse should act when interacting with park guests.
Amy Weir
My high school marching band did Magic Music Days at EPCOT, too, Patricia! But my best memory of that was later that evening, sitting by the lake in the dusk eating ice cream with my bandmates as we waited for the light show. That was also the trip where, at that same sombrero shop in Mexico, my friends convinced me to buy a straw sunhat (smaller than a proper sombrero though!) with a Minnie bow, that kind of became my signature after that and I've been partial to wide-brimmed sunhats ever since.
That was my middle visit to EPCOT: my first was in 1986, and I'm surprised there weren't any other trips in the middle, because my parents had bought a record album of EPCOT music that we listened to all the time after that, which probably helped cement my EPCOT memories and made them seem bigger. I was disappointed, when I dragged my high school friends to the food show in The Land Pavillion years later, that the produce no longer sang the "Veggie Veggie Fruit Fruit" song. Also, random songs from that album still pop into my head at odd moments today.
Last year we were there on my princess-loving daughter's 7th birthday, which seemed too well-timed not to splurge on the Princess Lunch in Norway: expensive, but so tasty! I'm not sure she was quite as into it as she could have been, though, because it turned out she was coming down with strep throat and kept falling asleep in lines the rest of the day. But my absolute favorite EPCOT memory has nothing to do with Disney-magic. Later that week, as my 9-year-old son and I stood in a line in a shop in Japan waiting for a candy sample, a worker in the next room spilled a box of hairpins on the floor. My son, who usually doesn't even clean up his own spills, impulsively jumped out of line and into the room to help her pick them up. I was so proud of that burst of kindness.OH, it was in EPCOT where I first met Mickey, too! Near MY birthday! And he wrote happy birthday to me in my autograph book!
Oh, it was in EPCOT where I first met Mickey, too! Near MY birthday! And he wrote happy birthday to me in my autograph book!
Anika Dane
I was six and I don't remember anything except getting in trouble for not finishing my dinner in "Germany." (I was six! It was weird!)
I was thirteen and my mother had died a few months before. I remember waiting in line to meet Space Mickey and Minnie with my five-year-old brother.
I was seventeen and I'd just graduated high school. My best friend and I had lunch with Chip and Dale at The Land as part of a trip to Disney our parents sent us on, my first "adult" vacation (lol).
I was twenty-two and my father had died a few months before, so we went to Disney World as what I now see as a traditional celebration of life and family. My daughter was not even a year old and later said it doesn't count as a trip to Disney if she remembers nothing and couldn't walk.
I was thirty and I dressed as Fleur Delacour to have a photoshoot in "France." That is probably my favorite memory of EPCOT.
I was almost thirty-six, almost one year older than my mother was when she died, and we went to Disney for my birthday. It was late December and freezing. Edward James Olmos narrated the Candlelight Processional.
I was forty and we only had two days at Disney World so we missed EPCOT. But the first night we were there, we took the monorail to the park so we could see the geosphere all lit up and it brought tears to my eyes. We'll go again soon. (I've been saving since we left!)
Filed Under: Featured, GeekMom, Travel
← Revisit EPCOT's Past With 12 Videos of Lost Attractions
Comic Book Corner: 4 Comics We Read in August & September 2017 →