-
Notifications
You must be signed in to change notification settings - Fork 0
/
inv1rel3.v
101 lines (97 loc) · 2.4 KB
/
inv1rel3.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
(* Contribution to the Coq Library V6.3 (July 1999) *)
Require Import securite.
Lemma POinv1rel3 :
forall (l l0 : list C) (k k0 k1 k2 : K) (c c0 c1 c2 : C)
(d d0 d1 d2 d3 d4 d5 d6 d7 d8 d9 d10 d11 d12 d13 d14 d15 d16 d17 d18 d19
d20 : D),
inv0
(ABSI (MBNaKab d7 d8 d9 k0) (MANbKabCaCb d4 d5 d6 k c c0)
(MABNaNbKeyK d d0 d1 d2 d3) l) ->
inv1
(ABSI (MBNaKab d7 d8 d9 k0) (MANbKabCaCb d4 d5 d6 k c c0)
(MABNaNbKeyK d d0 d1 d2 d3) l) ->
rel3
(ABSI (MBNaKab d7 d8 d9 k0) (MANbKabCaCb d4 d5 d6 k c c0)
(MABNaNbKeyK d d0 d1 d2 d3) l)
(ABSI (MBNaKab d18 d19 d20 k2) (MANbKabCaCb d15 d16 d17 k1 c1 c2)
(MABNaNbKeyK d10 d11 d12 d13 d14) l0) ->
inv1
(ABSI (MBNaKab d18 d19 d20 k2) (MANbKabCaCb d15 d16 d17 k1 c1 c2)
(MABNaNbKeyK d10 d11 d12 d13 d14) l0).
Proof.
do 32 intro.
unfold inv0, inv1, rel3 in |- *.
intros know_c_c0_l know_Kas_Kbs and1.
elim know_Kas_Kbs; intros know_Kas know_Kbs.
elim and1; intros eq_l0 t1.
clear know_Kas_Kbs and1 t1.
split.
(* First part *)
apply D2.
rewrite eq_l0.
unfold quint in |- *.
simpl in |- *.
repeat apply C2 || apply C3 || apply C4.
apply
equivncomp
with
(Encrypt
(quad (B2C (D2B d17)) (B2C (D2B d4)) (B2C (D2B d16)) (B2C (D2B Bid)))
(KeyX Bid) :: c :: l ++ rngDDKKeyAB).
auto with otway_rees.
unfold quad in |- *.
repeat apply C2 || apply C3 || apply C4.
elim know_c_c0_l; intros know_c_l t.
apply equivncomp with (l ++ rngDDKKeyAB).
apply AlreadyIn; apply EP0; assumption.
apply D1; assumption.
discriminate.
discriminate.
discriminate.
discriminate.
discriminate.
discriminate.
discriminate.
discriminate.
discriminate.
discriminate.
discriminate.
discriminate.
discriminate.
discriminate.
discriminate.
(* second part *)
apply D2.
rewrite eq_l0.
unfold quint in |- *.
simpl in |- *.
repeat apply C2 || apply C3 || apply C4.
apply
equivncomp
with
(Encrypt
(quad (B2C (D2B d17)) (B2C (D2B d4)) (B2C (D2B d16)) (B2C (D2B Bid)))
(KeyX Bid) :: c :: l ++ rngDDKKeyAB).
auto with otway_rees.
unfold quad in |- *.
repeat apply C2 || apply C3 || apply C4.
elim know_c_c0_l; intros know_c_l t.
apply equivncomp with (l ++ rngDDKKeyAB).
apply AlreadyIn; apply EP0; assumption.
apply D1; assumption.
discriminate.
discriminate.
discriminate.
discriminate.
discriminate.
discriminate.
discriminate.
discriminate.
discriminate.
discriminate.
discriminate.
discriminate.
discriminate.
discriminate.
discriminate.
Qed.