Contribution: OtwayRees
Library OtwayRees.securite
Require Export List.
Parameter N : Set.
Inductive K : Set :=
| inv : K -> K
| ka : securite.N -> K
| ks : securite.N -> K.
Parameter D : Set.
Parameter Aid Bid : D.
Axiom
D_dec :
forall d1 d2 : D, {d1 = Aid /\ d2 = Bid} + {~ (d1 = Aid /\ d2 = Bid)}.
Inductive B : Set :=
| K2B : K -> B
| D2B : D -> B.
Inductive C : Set :=
| Encrypt : C -> K -> C
| Pair : C -> C -> C
| B2C : B -> C.
Notation SS := (list C) (only parsing).
Inductive known_in : C -> list C -> Prop :=
| E0 :
forall (c1 c2 : C) (s : list C), known_in c1 s -> known_in c1 (c2 :: s)
| EP0 :
forall (c : C) (s1 s2 : list C), known_in c s1 -> known_in c (s1 ++ s2)
| A1 :
forall (c1 c2 : C) (s : list C),
known_in c1 s -> known_in c2 s -> known_in (Pair c1 c2) s
| A2A :
forall (c1 c2 : C) (s : list C),
known_in (Pair c1 c2) s -> known_in c1 s
| A2B :
forall (c1 c2 : C) (s : list C),
known_in (Pair c1 c2) s -> known_in c2 s
| A3 :
forall (c1 : C) (k1 : K) (s : list C),
known_in c1 s ->
known_in (B2C (K2B k1)) s -> known_in (Encrypt c1 k1) s
| A4 :
forall (c1 : C) (k1 : K) (s : list C),
known_in (Encrypt c1 k1) s ->
known_in (B2C (K2B (inv k1))) s -> known_in c1 s.
Hint Resolve A1 A2A A2B A3 A4: otway_rees.
Inductive equivS : list C -> list C -> Prop :=
| equivS1a : equivS nil nil
| equivS1b :
forall (s1 s2 : list C) (c : C),
equivS s1 s2 -> equivS (c :: s1) (c :: s2)
| equivS2 :
forall (s : list C) (c1 c2 : C), equivS (c1 :: c2 :: s) (c2 :: c1 :: s)
| equivS4 :
forall s1 s2 s3 : list C, equivS s1 s2 -> equivS s2 s3 -> equivS s1 s3
| AlreadyIn1 : forall (c1 : C) (s : list C), In c1 s -> equivS s (c1 :: s)
| AlreadyIn1b : forall (c1 : C) (s : list C), In c1 s -> equivS (c1 :: s) s
| AlreadyIn :
forall (c1 : C) (s : list C), known_in c1 s -> equivS s (c1 :: s)
| AlreadyInb :
forall (c1 : C) (s : list C), known_in c1 s -> equivS (c1 :: s) s.
Hint Resolve equivS1a equivS1b equivS2 equivS4 AlreadyIn1 AlreadyIn1b
AlreadyIn AlreadyInb: otway_rees.
Lemma equivS3 : forall s1 s2 : list C, equivS s1 s2 -> equivS s2 s1.
Proof.
intros s1 s2 equiv; elim equiv; eauto with otway_rees v62.
Qed.
Fixpoint setofkeys (s : list C) : Prop :=
match s with
| nil => True
| B2C (K2B _) :: s1 => setofkeys s1
| _ => False
end.
Inductive not_comp_of : C -> list C -> Prop :=
| C1 :
forall (c1 c2 : C) (k : K) (s : list C),
not_comp_of (B2C (K2B k)) s ->
c1 <> Encrypt c2 k -> not_comp_of c1 (Encrypt c2 k :: s)
| C2 :
forall (c1 c2 : C) (k : K) (s : list C),
not_comp_of c1 (c2 :: s) ->
c1 <> Encrypt c2 k -> not_comp_of c1 (Encrypt c2 k :: s)
| C3 :
forall (c1 : C) (d : D) (s : list C),
not_comp_of c1 s ->
c1 <> B2C (D2B d) -> not_comp_of c1 (B2C (D2B d) :: s)
| C4 :
forall (c1 c2 c3 : C) (s : list C),
not_comp_of c1 (c2 :: c3 :: s) ->
c1 <> Pair c2 c3 -> not_comp_of c1 (Pair c2 c3 :: s)
| C5 : forall c1 : C, not_comp_of c1 nil
| C7 :
forall (k : K) (s : list C),
~ In (B2C (K2B k)) s -> setofkeys s -> not_comp_of (B2C (K2B k)) s
| D1 : forall (c1 : C) (s : list C), ~ known_in c1 s -> not_comp_of c1 s
| UnionSnE1 :
forall (c : C) (s1 s2 : list C),
not_comp_of c (s1 ++ s2) -> not_comp_of c s1.
Axiom
D2 :
forall (b : B) (s : list C),
not_comp_of (B2C b) s -> ~ known_in (B2C b) s.
Axiom
E1 :
forall (c1 c2 : C) (s : list C),
~ known_in c1 (c2 :: s) -> ~ known_in c1 s.
Axiom
EP1 :
forall (c : C) (s1 s2 : list C),
~ known_in c (s1 ++ s2) -> ~ known_in c s1.
Hint Resolve C1 C2 C3 C4 C5 C7 D1 UnionSnE1 D2 E1 EP1: otway_rees.
Axiom
equivknown :
forall (c : C) (s1 s2 : list C),
equivS s1 s2 -> known_in c s1 -> known_in c s2.
Axiom
equivncomp :
forall (c : C) (s1 s2 : list C),
equivS s1 s2 -> not_comp_of c s1 -> not_comp_of c s2.
Lemma equivnknown1 :
forall (c1 c2 : C) (s1 s2 : list C),
equivS s1 s2 -> c1 = c2 -> ~ known_in c1 s1 -> ~ known_in c2 s2.
Proof.
intros.
elim H0.
unfold not in |- *; intros.
apply H1.
apply (equivknown c1 s2 s1).
elim H; simpl in |- *; eauto with otway_rees v62.
exact H2.
Qed.
Parameter KeyAB : D -> D -> K.
Parameter KeyX : D -> K.
Parameter rngDDKKeyAB : list C.
Parameter rngDDKKeyABminusKab : list C.
Axiom rngs : equivS rngDDKKeyAB (rngDDKKeyABminusKab ++ rngDDKKeyAB).
Notation Kab := (KeyAB Aid Bid) (only parsing).
Notation Kas := (KeyX Aid) (only parsing).
Notation Kbs := (KeyX Bid) (only parsing).
Axiom disjKasKeyAB : forall d1 d2 : D, KeyAB d1 d2 <> KeyX Aid.
Axiom
rngDDKKeyAB1 : forall d1 d2 : D, In (B2C (K2B (KeyAB d1 d2))) rngDDKKeyAB.
Axiom
rngDDKKeyABminusKab1 :
forall d1 d2 : D,
KeyAB d1 d2 <> KeyAB Aid Bid ->
In (B2C (K2B (KeyAB d1 d2))) rngDDKKeyABminusKab.
Axiom
KeyAB1 :
forall d1 d2 : D,
~ (d1 = Aid /\ d2 = Bid) -> KeyAB d1 d2 <> KeyAB Aid Bid.
Definition triple (c1 c2 c3 : C) := Pair c1 (Pair c2 c3).
Definition quad (c1 c2 c3 c4 : C) := Pair c1 (Pair c2 (Pair c3 c4)).
Definition quint (c1 c2 c3 c4 c5 : C) :=
Pair c1 (Pair c2 (Pair c3 (Pair c4 c5))).
Definition new (n : D) (s : list C) :=
forall s2 : list C, setofkeys s2 -> ~ known_in (B2C (D2B n)) (s ++ s2).
Inductive AState : Set :=
MBNaKab : D -> D -> D -> K -> AState.
Inductive BState : Set :=
MANbKabCaCb : D -> D -> D -> K -> C -> C -> BState.
Inductive SState : Set :=
MABNaNbKeyK : D -> D -> D -> D -> D -> SState.
Inductive GlobalState : Set :=
ABSI : AState -> BState -> SState -> list C -> GlobalState.
Definition inv0 (st : GlobalState) :=
match st with
| ABSI _ (MANbKabCaCb _ _ _ _ ca cb) _ s => known_in ca s /\ known_in cb s
end.
Definition inv1 (st : GlobalState) :=
match st with
| ABSI _ _ _ s =>
~ known_in (B2C (K2B (KeyX Aid))) (s ++ rngDDKKeyAB) /\
~ known_in (B2C (K2B (KeyX Bid))) (s ++ rngDDKKeyAB)
end.
Definition invP (st : GlobalState) :=
match st with
| ABSI _ _ _ s =>
~ known_in (B2C (K2B (KeyAB Aid Bid))) (s ++ rngDDKKeyABminusKab)
end.
Definition rel1 (st1 st2 : GlobalState) :=
match st1, st2 with
| ABSI sta1 stb1 sts1 s1, ABSI sta2 stb2 sts2 s2 =>
match sta1, sta2 with
| MBNaKab _ _ na1 kab1, MBNaKab m2 b2 na2 kab2 =>
s2 =
quad (B2C (D2B m2)) (B2C (D2B Aid)) (B2C (D2B b2))
(Encrypt
(quad (B2C (D2B na2)) (B2C (D2B m2))
(B2C (D2B Aid)) (B2C (D2B b2))) (KeyX Aid)) :: s1 /\
new na2 s1 /\
new m2 s1 /\ stb1 = stb2 /\ sts1 = sts2 /\ na1 = na2 /\ kab1 = kab2
end
end.
Definition rel2 (st1 st2 : GlobalState) :=
match st1, st2 with
| ABSI sta1 stb1 sts1 s1, ABSI sta2 stb2 sts2 s2 =>
match stb1, stb2 with
| MANbKabCaCb _ _ nb1 kab1 _ cb1, MANbKabCaCb m2 a2 nb2 kab2 ca2 cb2 =>
known_in (quad (B2C (D2B m2)) (B2C (D2B a2)) (B2C (D2B Bid)) ca2)
s1 /\
sta1 = sta2 /\
sts1 = sts2 /\ s1 = s2 /\ nb1 = nb2 /\ kab1 = kab2 /\ cb1 = cb2
end
end.
Definition rel3 (st1 st2 : GlobalState) :=
match st1, st2 with
| ABSI sta1 stb1 sts1 s1, ABSI sta2 stb2 sts2 s2 =>
match stb1, stb2 with
| MANbKabCaCb m1 a1 nb1 kab1 ca1 cb1, MANbKabCaCb m2 a2 nb2 kab2 ca2
cb2 =>
s2 =
quint (B2C (D2B m1)) (B2C (D2B a1)) (B2C (D2B Bid)) ca1
(Encrypt
(quad (B2C (D2B nb2)) (B2C (D2B m1))
(B2C (D2B a2)) (B2C (D2B Bid))) (KeyX Bid)) :: s1 /\
new nb2 s1 /\
sta1 = sta2 /\
sts1 = sts2 /\
m1 = m2 /\ a1 = a2 /\ kab1 = kab2 /\ ca1 = ca2 /\ cb1 = cb2
end
end.
Definition rel4 (st1 st2 : GlobalState) :=
match st1, st2 with
| ABSI sta1 stb1 _ s1, ABSI sta2 stb2 sts2 s2 =>
match sts2 with
| MABNaNbKeyK m2 a2 b2 na2 nb2 =>
known_in
(quint (B2C (D2B m2)) (B2C (D2B a2)) (B2C (D2B b2))
(Encrypt
(quad (B2C (D2B na2)) (B2C (D2B m2))
(B2C (D2B a2)) (B2C (D2B b2)))
(KeyX a2))
(Encrypt
(quad (B2C (D2B nb2)) (B2C (D2B m2))
(B2C (D2B a2)) (B2C (D2B b2)))
(KeyX b2))) s1 /\ sta1 = sta2 /\ stb1 = stb2 /\ s1 = s2
end
end.
Definition rel5 (st1 st2 : GlobalState) :=
match st1, st2 with
| ABSI sta1 stb1 sts1 s1, ABSI sta2 stb2 sts2 s2 =>
match sts1 with
| MABNaNbKeyK m1 a1 b1 na1 nb1 =>
s2 =
triple (B2C (D2B m1))
(Encrypt (Pair (B2C (D2B na1)) (B2C (K2B (KeyAB a1 b1))))
(KeyX a1))
(Encrypt (Pair (B2C (D2B nb1)) (B2C (K2B (KeyAB a1 b1))))
(KeyX b1)) :: s1 /\ sta1 = sta2 /\ stb1 = stb2 /\ sts1 = sts2
end
end.
Definition rel6 (st1 st2 : GlobalState) :=
match st1, st2 with
| ABSI sta1 stb1 sts1 s1, ABSI sta2 stb2 sts2 s2 =>
match stb1, stb2 with
| MANbKabCaCb m1 a1 nb1 _ ca1 _, MANbKabCaCb m2 a2 nb2 kab2 ca2 cb2 =>
known_in
(triple (B2C (D2B m1)) cb2
(Encrypt (Pair (B2C (D2B nb1)) (B2C (K2B kab2))) (KeyX Bid)))
s1 /\
sta1 = sta2 /\
sts1 = sts2 /\
s1 = s2 /\ m1 = m2 /\ a1 = a2 /\ nb1 = nb2 /\ ca1 = ca2
end
end.
Definition rel7 (st1 st2 : GlobalState) :=
match st1, st2 with
| ABSI sta1 stb1 sts1 s1, ABSI sta2 stb2 sts2 s2 =>
match stb1 with
| MANbKabCaCb m1 _ _ _ _ cb1 =>
s2 = Pair (B2C (D2B m1)) cb1 :: s1 /\
sta1 = sta2 /\ stb1 = stb2 /\ sts1 = sts2
end
end.
Definition rel8 (st1 st2 : GlobalState) :=
match st1, st2 with
| ABSI sta1 stb1 sts1 s1, ABSI sta2 stb2 sts2 s2 =>
match sta1, sta2 with
| MBNaKab m1 b1 na1 _, MBNaKab m2 b2 na2 kab2 =>
known_in
(Pair (B2C (D2B m1))
(Encrypt (Pair (B2C (D2B na1)) (B2C (K2B kab2))) (KeyX Aid)))
s1 /\
stb1 = stb2 /\
sts1 = sts2 /\ s1 = s2 /\ m1 = m2 /\ b1 = b2 /\ na1 = na2
end
end.
Definition rel (st1 st2 : GlobalState) :=
rel1 st1 st2 \/
rel2 st1 st2 \/
rel3 st1 st2 \/
rel4 st1 st2 \/
rel5 st1 st2 \/ rel6 st1 st2 \/ rel7 st1 st2 \/ rel8 st1 st2.
Parameter N : Set.
Inductive K : Set :=
| inv : K -> K
| ka : securite.N -> K
| ks : securite.N -> K.
Parameter D : Set.
Parameter Aid Bid : D.
Axiom
D_dec :
forall d1 d2 : D, {d1 = Aid /\ d2 = Bid} + {~ (d1 = Aid /\ d2 = Bid)}.
Inductive B : Set :=
| K2B : K -> B
| D2B : D -> B.
Inductive C : Set :=
| Encrypt : C -> K -> C
| Pair : C -> C -> C
| B2C : B -> C.
Notation SS := (list C) (only parsing).
Inductive known_in : C -> list C -> Prop :=
| E0 :
forall (c1 c2 : C) (s : list C), known_in c1 s -> known_in c1 (c2 :: s)
| EP0 :
forall (c : C) (s1 s2 : list C), known_in c s1 -> known_in c (s1 ++ s2)
| A1 :
forall (c1 c2 : C) (s : list C),
known_in c1 s -> known_in c2 s -> known_in (Pair c1 c2) s
| A2A :
forall (c1 c2 : C) (s : list C),
known_in (Pair c1 c2) s -> known_in c1 s
| A2B :
forall (c1 c2 : C) (s : list C),
known_in (Pair c1 c2) s -> known_in c2 s
| A3 :
forall (c1 : C) (k1 : K) (s : list C),
known_in c1 s ->
known_in (B2C (K2B k1)) s -> known_in (Encrypt c1 k1) s
| A4 :
forall (c1 : C) (k1 : K) (s : list C),
known_in (Encrypt c1 k1) s ->
known_in (B2C (K2B (inv k1))) s -> known_in c1 s.
Hint Resolve A1 A2A A2B A3 A4: otway_rees.
Inductive equivS : list C -> list C -> Prop :=
| equivS1a : equivS nil nil
| equivS1b :
forall (s1 s2 : list C) (c : C),
equivS s1 s2 -> equivS (c :: s1) (c :: s2)
| equivS2 :
forall (s : list C) (c1 c2 : C), equivS (c1 :: c2 :: s) (c2 :: c1 :: s)
| equivS4 :
forall s1 s2 s3 : list C, equivS s1 s2 -> equivS s2 s3 -> equivS s1 s3
| AlreadyIn1 : forall (c1 : C) (s : list C), In c1 s -> equivS s (c1 :: s)
| AlreadyIn1b : forall (c1 : C) (s : list C), In c1 s -> equivS (c1 :: s) s
| AlreadyIn :
forall (c1 : C) (s : list C), known_in c1 s -> equivS s (c1 :: s)
| AlreadyInb :
forall (c1 : C) (s : list C), known_in c1 s -> equivS (c1 :: s) s.
Hint Resolve equivS1a equivS1b equivS2 equivS4 AlreadyIn1 AlreadyIn1b
AlreadyIn AlreadyInb: otway_rees.
Lemma equivS3 : forall s1 s2 : list C, equivS s1 s2 -> equivS s2 s1.
Proof.
intros s1 s2 equiv; elim equiv; eauto with otway_rees v62.
Qed.
Fixpoint setofkeys (s : list C) : Prop :=
match s with
| nil => True
| B2C (K2B _) :: s1 => setofkeys s1
| _ => False
end.
Inductive not_comp_of : C -> list C -> Prop :=
| C1 :
forall (c1 c2 : C) (k : K) (s : list C),
not_comp_of (B2C (K2B k)) s ->
c1 <> Encrypt c2 k -> not_comp_of c1 (Encrypt c2 k :: s)
| C2 :
forall (c1 c2 : C) (k : K) (s : list C),
not_comp_of c1 (c2 :: s) ->
c1 <> Encrypt c2 k -> not_comp_of c1 (Encrypt c2 k :: s)
| C3 :
forall (c1 : C) (d : D) (s : list C),
not_comp_of c1 s ->
c1 <> B2C (D2B d) -> not_comp_of c1 (B2C (D2B d) :: s)
| C4 :
forall (c1 c2 c3 : C) (s : list C),
not_comp_of c1 (c2 :: c3 :: s) ->
c1 <> Pair c2 c3 -> not_comp_of c1 (Pair c2 c3 :: s)
| C5 : forall c1 : C, not_comp_of c1 nil
| C7 :
forall (k : K) (s : list C),
~ In (B2C (K2B k)) s -> setofkeys s -> not_comp_of (B2C (K2B k)) s
| D1 : forall (c1 : C) (s : list C), ~ known_in c1 s -> not_comp_of c1 s
| UnionSnE1 :
forall (c : C) (s1 s2 : list C),
not_comp_of c (s1 ++ s2) -> not_comp_of c s1.
Axiom
D2 :
forall (b : B) (s : list C),
not_comp_of (B2C b) s -> ~ known_in (B2C b) s.
Axiom
E1 :
forall (c1 c2 : C) (s : list C),
~ known_in c1 (c2 :: s) -> ~ known_in c1 s.
Axiom
EP1 :
forall (c : C) (s1 s2 : list C),
~ known_in c (s1 ++ s2) -> ~ known_in c s1.
Hint Resolve C1 C2 C3 C4 C5 C7 D1 UnionSnE1 D2 E1 EP1: otway_rees.
Axiom
equivknown :
forall (c : C) (s1 s2 : list C),
equivS s1 s2 -> known_in c s1 -> known_in c s2.
Axiom
equivncomp :
forall (c : C) (s1 s2 : list C),
equivS s1 s2 -> not_comp_of c s1 -> not_comp_of c s2.
Lemma equivnknown1 :
forall (c1 c2 : C) (s1 s2 : list C),
equivS s1 s2 -> c1 = c2 -> ~ known_in c1 s1 -> ~ known_in c2 s2.
Proof.
intros.
elim H0.
unfold not in |- *; intros.
apply H1.
apply (equivknown c1 s2 s1).
elim H; simpl in |- *; eauto with otway_rees v62.
exact H2.
Qed.
Parameter KeyAB : D -> D -> K.
Parameter KeyX : D -> K.
Parameter rngDDKKeyAB : list C.
Parameter rngDDKKeyABminusKab : list C.
Axiom rngs : equivS rngDDKKeyAB (rngDDKKeyABminusKab ++ rngDDKKeyAB).
Notation Kab := (KeyAB Aid Bid) (only parsing).
Notation Kas := (KeyX Aid) (only parsing).
Notation Kbs := (KeyX Bid) (only parsing).
Axiom disjKasKeyAB : forall d1 d2 : D, KeyAB d1 d2 <> KeyX Aid.
Axiom
rngDDKKeyAB1 : forall d1 d2 : D, In (B2C (K2B (KeyAB d1 d2))) rngDDKKeyAB.
Axiom
rngDDKKeyABminusKab1 :
forall d1 d2 : D,
KeyAB d1 d2 <> KeyAB Aid Bid ->
In (B2C (K2B (KeyAB d1 d2))) rngDDKKeyABminusKab.
Axiom
KeyAB1 :
forall d1 d2 : D,
~ (d1 = Aid /\ d2 = Bid) -> KeyAB d1 d2 <> KeyAB Aid Bid.
Definition triple (c1 c2 c3 : C) := Pair c1 (Pair c2 c3).
Definition quad (c1 c2 c3 c4 : C) := Pair c1 (Pair c2 (Pair c3 c4)).
Definition quint (c1 c2 c3 c4 c5 : C) :=
Pair c1 (Pair c2 (Pair c3 (Pair c4 c5))).
Definition new (n : D) (s : list C) :=
forall s2 : list C, setofkeys s2 -> ~ known_in (B2C (D2B n)) (s ++ s2).
Inductive AState : Set :=
MBNaKab : D -> D -> D -> K -> AState.
Inductive BState : Set :=
MANbKabCaCb : D -> D -> D -> K -> C -> C -> BState.
Inductive SState : Set :=
MABNaNbKeyK : D -> D -> D -> D -> D -> SState.
Inductive GlobalState : Set :=
ABSI : AState -> BState -> SState -> list C -> GlobalState.
Definition inv0 (st : GlobalState) :=
match st with
| ABSI _ (MANbKabCaCb _ _ _ _ ca cb) _ s => known_in ca s /\ known_in cb s
end.
Definition inv1 (st : GlobalState) :=
match st with
| ABSI _ _ _ s =>
~ known_in (B2C (K2B (KeyX Aid))) (s ++ rngDDKKeyAB) /\
~ known_in (B2C (K2B (KeyX Bid))) (s ++ rngDDKKeyAB)
end.
Definition invP (st : GlobalState) :=
match st with
| ABSI _ _ _ s =>
~ known_in (B2C (K2B (KeyAB Aid Bid))) (s ++ rngDDKKeyABminusKab)
end.
Definition rel1 (st1 st2 : GlobalState) :=
match st1, st2 with
| ABSI sta1 stb1 sts1 s1, ABSI sta2 stb2 sts2 s2 =>
match sta1, sta2 with
| MBNaKab _ _ na1 kab1, MBNaKab m2 b2 na2 kab2 =>
s2 =
quad (B2C (D2B m2)) (B2C (D2B Aid)) (B2C (D2B b2))
(Encrypt
(quad (B2C (D2B na2)) (B2C (D2B m2))
(B2C (D2B Aid)) (B2C (D2B b2))) (KeyX Aid)) :: s1 /\
new na2 s1 /\
new m2 s1 /\ stb1 = stb2 /\ sts1 = sts2 /\ na1 = na2 /\ kab1 = kab2
end
end.
Definition rel2 (st1 st2 : GlobalState) :=
match st1, st2 with
| ABSI sta1 stb1 sts1 s1, ABSI sta2 stb2 sts2 s2 =>
match stb1, stb2 with
| MANbKabCaCb _ _ nb1 kab1 _ cb1, MANbKabCaCb m2 a2 nb2 kab2 ca2 cb2 =>
known_in (quad (B2C (D2B m2)) (B2C (D2B a2)) (B2C (D2B Bid)) ca2)
s1 /\
sta1 = sta2 /\
sts1 = sts2 /\ s1 = s2 /\ nb1 = nb2 /\ kab1 = kab2 /\ cb1 = cb2
end
end.
Definition rel3 (st1 st2 : GlobalState) :=
match st1, st2 with
| ABSI sta1 stb1 sts1 s1, ABSI sta2 stb2 sts2 s2 =>
match stb1, stb2 with
| MANbKabCaCb m1 a1 nb1 kab1 ca1 cb1, MANbKabCaCb m2 a2 nb2 kab2 ca2
cb2 =>
s2 =
quint (B2C (D2B m1)) (B2C (D2B a1)) (B2C (D2B Bid)) ca1
(Encrypt
(quad (B2C (D2B nb2)) (B2C (D2B m1))
(B2C (D2B a2)) (B2C (D2B Bid))) (KeyX Bid)) :: s1 /\
new nb2 s1 /\
sta1 = sta2 /\
sts1 = sts2 /\
m1 = m2 /\ a1 = a2 /\ kab1 = kab2 /\ ca1 = ca2 /\ cb1 = cb2
end
end.
Definition rel4 (st1 st2 : GlobalState) :=
match st1, st2 with
| ABSI sta1 stb1 _ s1, ABSI sta2 stb2 sts2 s2 =>
match sts2 with
| MABNaNbKeyK m2 a2 b2 na2 nb2 =>
known_in
(quint (B2C (D2B m2)) (B2C (D2B a2)) (B2C (D2B b2))
(Encrypt
(quad (B2C (D2B na2)) (B2C (D2B m2))
(B2C (D2B a2)) (B2C (D2B b2)))
(KeyX a2))
(Encrypt
(quad (B2C (D2B nb2)) (B2C (D2B m2))
(B2C (D2B a2)) (B2C (D2B b2)))
(KeyX b2))) s1 /\ sta1 = sta2 /\ stb1 = stb2 /\ s1 = s2
end
end.
Definition rel5 (st1 st2 : GlobalState) :=
match st1, st2 with
| ABSI sta1 stb1 sts1 s1, ABSI sta2 stb2 sts2 s2 =>
match sts1 with
| MABNaNbKeyK m1 a1 b1 na1 nb1 =>
s2 =
triple (B2C (D2B m1))
(Encrypt (Pair (B2C (D2B na1)) (B2C (K2B (KeyAB a1 b1))))
(KeyX a1))
(Encrypt (Pair (B2C (D2B nb1)) (B2C (K2B (KeyAB a1 b1))))
(KeyX b1)) :: s1 /\ sta1 = sta2 /\ stb1 = stb2 /\ sts1 = sts2
end
end.
Definition rel6 (st1 st2 : GlobalState) :=
match st1, st2 with
| ABSI sta1 stb1 sts1 s1, ABSI sta2 stb2 sts2 s2 =>
match stb1, stb2 with
| MANbKabCaCb m1 a1 nb1 _ ca1 _, MANbKabCaCb m2 a2 nb2 kab2 ca2 cb2 =>
known_in
(triple (B2C (D2B m1)) cb2
(Encrypt (Pair (B2C (D2B nb1)) (B2C (K2B kab2))) (KeyX Bid)))
s1 /\
sta1 = sta2 /\
sts1 = sts2 /\
s1 = s2 /\ m1 = m2 /\ a1 = a2 /\ nb1 = nb2 /\ ca1 = ca2
end
end.
Definition rel7 (st1 st2 : GlobalState) :=
match st1, st2 with
| ABSI sta1 stb1 sts1 s1, ABSI sta2 stb2 sts2 s2 =>
match stb1 with
| MANbKabCaCb m1 _ _ _ _ cb1 =>
s2 = Pair (B2C (D2B m1)) cb1 :: s1 /\
sta1 = sta2 /\ stb1 = stb2 /\ sts1 = sts2
end
end.
Definition rel8 (st1 st2 : GlobalState) :=
match st1, st2 with
| ABSI sta1 stb1 sts1 s1, ABSI sta2 stb2 sts2 s2 =>
match sta1, sta2 with
| MBNaKab m1 b1 na1 _, MBNaKab m2 b2 na2 kab2 =>
known_in
(Pair (B2C (D2B m1))
(Encrypt (Pair (B2C (D2B na1)) (B2C (K2B kab2))) (KeyX Aid)))
s1 /\
stb1 = stb2 /\
sts1 = sts2 /\ s1 = s2 /\ m1 = m2 /\ b1 = b2 /\ na1 = na2
end
end.
Definition rel (st1 st2 : GlobalState) :=
rel1 st1 st2 \/
rel2 st1 st2 \/
rel3 st1 st2 \/
rel4 st1 st2 \/
rel5 st1 st2 \/ rel6 st1 st2 \/ rel7 st1 st2 \/ rel8 st1 st2.