Abstract Rewriting Challenge (Cops) This is a somewhat proof-golf-like cops-and-robbers challenge. This is the cops' thread; the robbers' thread is here.

Cops

Your task is to define an abstract rewriting system in which the reachability of one word from another is difficult to determine. You will prepare the following things:


A set of symbols, called the alphabet. (You may use any Unicode characters for these, but please don't use whitespace, or symbols that are hard to distinguish from each other.)
A source string composed of symbols from your alphabet.
A target string composed of symbols from your alphabet.
A set of rewrite rules using characters from your alphabet. (See below for the definition of a rewrite rule.)
A proof showing whether your source string can be converted into your target string by successive application of your rewrite rules. This proof might consist of an actual sequence of rewrite steps, or a mathematical proof that such a sequence must exist, or a mathematical proof that such a sequence does not exist.


You will post the first four of these, keeping the proof secret; the robbers will try to crack your answer by providing their own proof that your target string can or can not be reached from your source string. If your submission is not cracked within two weeks, you may mark it as safe and edit in your proof.

Submissions will be scored according to the number of characters in their rewrite rules and their source and target strings, as detailed below. The winner will be the uncracked submission with the lowest score.

What is a rewrite rule?

A rewrite rule is simply a pair of strings in your alphabet. (Either of these strings may be empty.) An application of a rewrite rule consists of finding a substring that is equal to the first string in the pair, and replacing it with the second. 

An example should make this clear:

Suppose alphabet is A, B and C; the source string is "A"; the target string is "C" and the rewrite rules are

A:B
B:BB
B:A
AA:C


then the target string is reachable in the following way:

A
B   (using rule 1)
BB  (using rule 2)
AB  (using rule 3)
AA  (using rule 3)
C   (using rule 4)


Scoring

Your score will be


the length of your source string, 
plus the length of your target string, 
plus the length of all the strings included in your rewrite rules, 
plus one extra point for each rewrite rule.


If you write your rewrite rules with a colon separator as above, this is just the total length of all the rewrite rules (including the separator), plus the lengths of the source and target strings. A lower score is better. The number of distinct characters in your alphabet will be used to break ties, with fewer being better.

Bounty

I'd like to see answers that really go for low scores. I will award 200 rep to the first answer that scores less than 100 points in this challenge and doesn't get cracked.
326 points - Cracked by jimmy23013
The level is Picokosmos #13 by Aymeric du Peloux (with a trivial modification). I tried to find a tasteful level that could be implemented with &quot;boxes&quot; and &quot;walls&quot; being the same character. For this level it was possible by making the central choke point two columns wide rather than one.
The rules/initial/target strings could be golfed a bit more, but this is just for fun.
Initial string:
___##___####_____##_#_#_##_#_!####______##_#####__####_#_######__###__

Target string:
___##___####_____##_#_#_##_#_#####____!__#_#####__####_#_######__###__

Rules:
_wW:!
_&lt;:&lt;_
Vv_:!
V_:_V
R:&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;&gt;
V#:#V
#w&lt;:w#
&gt;v_:_v
_wX:#
_!:!_
!:wLW_
L:&lt;&lt;&lt;&lt;&lt;&lt;&lt;&lt;&lt;&lt;&lt;&lt;&lt;
#W:W#
!#_:_!#
_w&lt;:w_
#&lt;:&lt;#
!:_VRv
&gt;v#:#v
Uv_:#
_W:W_
_X:X_
&gt;#:#&gt;
#X:X#
U_:_U
Vv#:!URv
#wW:wLX!
&gt;_:_&gt;
!_:_!
_#!:#!_
U#:#U