a_init(_n, _x) -> Node(_n) & name(_x)
a_init(_n, _x) & a_init(_n, _y) -> _x = _y
a_init(_n, _x) & Parent(_m, _n) -> a_init(_m, _x)
b_init(_n, _x) -> Node(_n) & name(_x)
b_init(_n, _x) & b_init(_n, _y) -> _x = _y
b_init(_n, _x) & Parent(_m, _n) -> b_init(_m, _x)
n1_init(_n, _x) -> Node(_n) & text(_x)
n1_init(_n, _x) & n1_init(_n, _y) -> _x = _y
n1_init(_n, _x) & Parent(_m, _n) -> n1_init(_m, _x)
n2_init(_n, _x) -> Node(_n) & text(_x)
n2_init(_n, _x) & n2_init(_n, _y) -> _x = _y
n2_init(_n, _x) & Parent(_m, _n) -> n2_init(_m, _x)
init1(_n) & n1_init(_n, n1) & a_init(_n, a) & b_init(_n, b) -> send(_n, Enc<Pair<n1, a>, Pubk<b>>)
init1(_n) -> Exists n1, a, b: n1_init(_n, n1) & a_init(_n, a) & b_init(_n, b)
init2(_n) & n1_init(_n, n1) & n2_init(_n, n2) & a_init(_n, a) -> recv(_n, Enc<Pair<n1, n2>, Pubk<a>>)
init2(_n) -> Exists _m: Parent(_n, _m) & init1(_m)
init2(_n) -> Exists n1, n2, a: n1_init(_n, n1) & n2_init(_n, n2) & a_init(_n, a)
init3(_n) & n2_init(_n, n2) & b_init(_n, b) -> send(_n, Enc<n2, Pubk<b>>)
init3(_n) -> Exists _m: Parent(_n, _m) & init2(_m)
init3(_n) -> Exists n2, b: n2_init(_n, n2) & b_init(_n, b)
a_resp(_n, _x) -> Node(_n) & name(_x)
a_resp(_n, _x) & a_resp(_n, _y) -> _x = _y
a_resp(_n, _x) & Parent(_m, _n) -> a_resp(_m, _x)
b_resp(_n, _x) -> Node(_n) & name(_x)
b_resp(_n, _x) & b_resp(_n, _y) -> _x = _y
b_resp(_n, _x) & Parent(_m, _n) -> b_resp(_m, _x)
n1_resp(_n, _x) -> Node(_n) & text(_x)
n1_resp(_n, _x) & n1_resp(_n, _y) -> _x = _y
n1_resp(_n, _x) & Parent(_m, _n) -> n1_resp(_m, _x)
n2_resp(_n, _x) -> Node(_n) & text(_x)
n2_resp(_n, _x) & n2_resp(_n, _y) -> _x = _y
n2_resp(_n, _x) & Parent(_m, _n) -> n2_resp(_m, _x)
resp1(_n) & n1_resp(_n, n1) & a_resp(_n, a) & b_resp(_n, b) -> recv(_n, Enc<Pair<n1, a>, Pubk<b>>)
resp1(_n) -> Exists n1, a, b: n1_resp(_n, n1) & a_resp(_n, a) & b_resp(_n, b)
resp2(_n) & n1_resp(_n, n1) & n2_resp(_n, n2) & a_resp(_n, a) -> send(_n, Enc<Pair<n1, n2>, Pubk<a>>)
resp2(_n) -> Exists _m: Parent(_n, _m) & resp1(_m)
resp2(_n) -> Exists n1, n2, a: n1_resp(_n, n1) & n2_resp(_n, n2) & a_resp(_n, a)
resp3(_n) & n2_resp(_n, n2) & b_resp(_n, b) -> recv(_n, Enc<n2, Pubk<b>>)
resp3(_n) -> Exists _m: Parent(_n, _m) & resp2(_m)
resp3(_n) -> Exists n2, b: n2_resp(_n, n2) & b_resp(_n, b)
True -> Exists _n0, a, b, n1: name(a) & name(b) & text(n1) & non-orig(Privk<b>) & non-orig(Privk<a>) & uniq-orig(n1) & init3(_n0) & a_init(_n0, a) & b_init(_n0, b) & n1_init(_n0, n1)
True -> Exists _n0, a, n2: name(a) & text(n2) & non-orig(Privk<a>) & uniq-orig(n2) & resp3(_n0) & a_resp(_n0, a) & n2_resp(_n0, n2)