INRIA_Internship/Sap_Tam/exclusive-secrets.spthy at master · dchandak99/INRIA_Internship · GitHub

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
102
103
104
105
106
107
108
109
110
111
theory ExclusiveSecrets
begin

functions: rep/2 [private], check_rep/2, get_rep/1
equations: check_rep(rep(m,loc),loc)=m, get_rep(rep(m,loc))=m

functions: store/0, left/0, right/0

//heuristic: p /* heuristic for SAPIC */

rule Init_: // [process=top-level] Init
 [] --[Init()]-> [State_()]

rule in_x_: // [process=top-level] in x
 [State_(), In(x)] --[]-> [State_1(x)]

rule insert_store_x_1: // [process=top-level] insert store,x
 [State_1(x)] --[Insert(store, x)]-> [State_11(x)]

rule event_SetStorex_11: // [process=top-level] event SetStore(x)
 [State_11(x)] --[Event(), SetStore(x)]-> [State_111(x)]

rule new_a_111: // [process=top-level] new a
 [State_111(x), Fr(a)] --[]-> [State_1111(a, x)]

rule new_b_1111: // [process=top-level] new b
 [State_1111(a, x), Fr(b)] --[]-> [State_11111(a, b, x)]

rule event_Secreta_b_11111: // [process=top-level] event Secret(a, b)
 [State_11111(a, b, x)] --[Event(), Secret(a, b)]-> [State_111111(a, b, x)]

rule Rep_0_111111: // [process=top-level] Rep, 0
 [State_111111(a, b, x)] --[]-> [!Semistate_1111111(a, b, x)]

rule Rep_1_111111: // [process=top-level] Rep, 1
 [!Semistate_1111111(a, b, x)] --[]-> [State_1111111(a, b, x)]

rule lookup_store_as_v_0_1111111 [color=#569DC0]: // [process=P] lookup store as v, 0
 [State_1111111(a, b, x)] --[IsIn(store, v)]-> [State_11111111(a, b, v, x)]

rule lookup_store_as_v_1_1111111 [color=#569DC0]: // [process=P] lookup store as v, 1
 [State_1111111(a, b, x)] --[IsNotSet(store)]-> [State_11111112(a, b, x)]

rule if_eqv_left_0_11111111 [color=#569DC0]: // [process=P] if eq(v, left()), 0
 [State_11111111(a, b, v, x)] --[Pred_eq(v, left())]-> [State_111111111(a, b, v, x)]

rule if_eqv_left_1_11111111 [color=#569DC0]: // [process=P] if eq(v, left()), 1
 [State_11111111(a, b, v, x)] --[Pred_not_eq(v, left())]-> [State_111111112(a, b, v, x)]

rule out_a_111111111 [color=#569DC0]: // [process=P] out a
 [State_111111111(a, b, v, x)] --[]-> [State_1111111111(a, b, v, x), Out(a)]

rule Zero_1111111111 [color=#569DC0]: // [process=P] Zero
 [State_1111111111(a, b, v, x)] --[]-> []

rule if_eqv_right_0_111111112 [color=#569DC0]: // [process=P] if eq(v, right()), 0
 [State_111111112(a, b, v, x)] --[Pred_eq(v, right())]-> [State_1111111121(a, b, v, x)]

rule if_eqv_right_1_111111112 [color=#569DC0]: // [process=P] if eq(v, right()), 1
 [State_111111112(a, b, v, x)] --[Pred_not_eq(v, right())]-> [State_1111111122(a, b, v, x)]

rule out_b_1111111121 [color=#569DC0]: // [process=P] out b
 [State_1111111121(a, b, v, x)] --[]-> [State_11111111211(a, b, v, x), Out(b)]

rule Zero_11111111211 [color=#569DC0]: // [process=P] Zero
 [State_11111111211(a, b, v, x)] --[]-> []

rule Zero_1111111122 [color=#569DC0]: // [process=P] Zero
 [State_1111111122(a, b, v, x)] --[]-> []

rule Zero_11111112 [color=#569DC0]: // [process=P] Zero
 [State_11111112(a, b, x)] --[]-> []

 restriction set_in:
"All x y #t3 . IsIn(x,y)@t3 ==>
        (Ex #t2 . Insert(x,y)@t2 & #t2<#t3
                & ( All #t1 . Delete(x)@t1 ==> (#t1<#t2 |  #t3<#t1))
                & ( All #t1 yp . Insert(x,yp)@t1 ==> (#t1<#t2 | #t1=#t2 | #t3<#t1))
)"

restriction set_notin:
"All x #t3 . IsNotSet(x)@t3 ==>
        (All #t1 y . Insert(x,y)@t1 ==>  #t3<#t1 )
  | ( Ex #t1 .   Delete(x)@t1 & #t1<#t3
                &  (All #t2 y . Insert(x,y)@t2 & #t2<#t3 ==>  #t2<#t1))"


restriction predicate_eq:
"All #i a b. Pred_eq(a,b)@i ==> a = b"


restriction predicate_not_eq:
"All #i a b. Pred_not_eq(a,b)@i ==> not(a = b)"


restriction single_session: // for a single session
    "All #i #j. Init()@i & Init()@j ==> #i=#j"

lemma a_not_secret : exists-trace
"	Ex #i #j x y. Secret(x, y) @ i & K(x) @ j"

lemma b_not_secret : exists-trace
"	Ex #i #j x y. Secret(x, y) @ i & K(y) @ j"

lemma sanity :
"	All #i #j #k x y z. Secret(x, y) @ i & K(x) @ j & SetStore(z) @ k ==> z = left"

lemma exclusive_secrets :
"	notEx #i #j #k x y. Secret(x, y) @ i & K(x) @ j & K(y) @ k"

end