-
Notifications
You must be signed in to change notification settings - Fork 1
Expand file tree
/
Copy pathrunning-ex-secrecy.html
More file actions
132 lines (113 loc) · 10.4 KB
/
running-ex-secrecy.html
File metadata and controls
132 lines (113 loc) · 10.4 KB
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
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
<!DOCTYPE html>
<html lang="en-US">
<head>
<meta charset="UTF-8">
<title>Squirrel Prover - Squirrel Prover</title>
<link rel="stylesheet" href="style.css">
</head>
<body onkeydown="key(event)">
<span style="display: none;"><span class="squirrel-step" id="step0">
<span class="input-line" id="in0">name s0 : index->message.</span>
<span class="output-line" id="out0"></span>
<span class="com-line" id="com0"><h1 id="running-example---secrecy">RUNNING EXAMPLE - secrecy</h1>
<p>In this file we illustrate the articulation between equivalence and reachability by showing a proof of (weak) secrecy using a strong secrecy property as hypothesis.</p>
<p>We first declare:</p>
<ul>
<li>an indexed name <code>s0(i)</code> used to initialize the mutable state <code>s</code>;</li>
<li>a name <code>m</code> used to represent a fresh random message.</li>
</ul>
</span>
</span>
<span class="squirrel-step" id="step1">
<span class="input-line" id="in1"><br>mutable s (i:index) : message = s0(i).</span>
<span class="output-line" id="out1"></span>
</span>
<span class="squirrel-step" id="step2">
<span class="input-line" id="in2"><br>name m : message.</span>
<span class="output-line" id="out2"></span>
</span>
<span class="squirrel-step" id="step3">
<span class="input-line" id="in3">system null.</span>
<span class="output-line" id="out3">System before processing:<br> <br> <span class="pn" style="font-weight:bold; color: #0000AA">null</span><br><br>System after processing:<br> <br> <span class="pn" style="font-weight:bold; color: #0000AA">null</span><br><br>System default registered with actions (init).<br></span>
<span class="com-line" id="com3"><p>In this file, our goal is to prove a secrecy property regardless of any specific protocol. This is why we declare an empty system.</p>
</span>
</span>
<span class="squirrel-step" id="step4">
<span class="input-line" id="in4">global goal [default/left,default/left] secrecy (i:index,tau,tau':timestamp):<br> [happens(pred(tau))]<br> -> equiv(frame@tau, diff(s(i)@tau',m))<br> -> [input@tau <> s(i)@tau'].</span>
<span class="output-line" id="out4">Goal secrecy :<br> forall i:index,tau,tau':timestamp,<br> [<span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="gf" style="font-weight: bold">pred</span>(tau))] -><br> equiv(<span class="gm" style="font-weight: bold; color: #AA00AA">frame</span>@tau, diff(<span class="gm" style="font-weight: bold; color: #AA00AA">s</span>(i)@tau', <span class="gn" style="color: #AA5500">m</span>)) -> [<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@tau <> <span class="gm" style="font-weight: bold; color: #AA00AA">s</span>(i)@tau']<br></span>
<span class="com-line" id="com4"><p>The following secrecy property is expressed by a global meta-logic formula. It states that, if the values stored in the memory cell <code>s</code> are strongly secret (this is expressed by the formula <code>equiv(frame@tau, diff(s(i)@tau',m))</code>), then the value <code>s(i)@tau'</code> is weakly secret, <em>i.e.</em> the attacker cannot deduce this value (this is expressed by the formula <code>[input@tau <> s(i)@tau']</code>).</p>
<p>Note that <code>happens(pred(tau))</code> is needed for the proof, and actually implies <code>happens(tau)</code>.</p>
<p>Note that this global meta-logic formula is defined w.r.t. the same system (<code>default/left</code>) for the left and the right projections. This is a technical restriction coming from the fact that, in the current implementation of Squirrel, global and local hypotheses cannot coexist.</p>
</span>
</span>
<span class="squirrel-step" id="step5">
<span class="input-line" id="in5">Proof.</span>
<span class="output-line" id="out5">[goal> Focused goal (1/1):<br>Systems: left:default/left, right:default/left (same for equivalences)<br>Variables: i:index,tau,tau':timestamp<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>[<span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="gf" style="font-weight: bold">pred</span>(tau))] -><br>equiv(<span class="gm" style="font-weight: bold; color: #AA00AA">frame</span>@tau, diff(<span class="gm" style="font-weight: bold; color: #AA00AA">s</span>(i)@tau', <span class="gn" style="color: #AA5500">m</span>)) -> [<span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@tau <> <span class="gm" style="font-weight: bold; color: #AA00AA">s</span>(i)@tau']<br><br></span>
<span class="com-line" id="com5"><p>The high-level idea of this proof is to use the strong secrecy hypothesis to prove the weak secrecy, relying on the <code>rewrite equiv</code> tactic which allows to derive a reachability judgement from an equivalence judgement.</p>
</span>
</span>
<span class="squirrel-step" id="step6">
<span class="input-line" id="in6"> intro Hap H.</span>
<span class="output-line" id="out6">[> Line 51: (intro Hap H) <br>[goal> Focused goal (1/1):<br>System: left:default/left, right:default/left (same for equivalences)<br>Variables: i:index,tau,tau':timestamp<br>H: equiv(<span class="gm" style="font-weight: bold; color: #AA00AA">frame</span>@tau, diff(<span class="gm" style="font-weight: bold; color: #AA00AA">s</span>(i)@tau', <span class="gn" style="color: #AA5500">m</span>))<br>Hap: [<span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="gf" style="font-weight: bold">pred</span>(tau))]<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br><span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@tau <> <span class="gm" style="font-weight: bold; color: #AA00AA">s</span>(i)@tau'<br><br></span>
<span class="com-line" id="com6"><p>We start by introducing the hypotheses.</p>
</span>
</span>
<span class="squirrel-step" id="step7">
<span class="input-line" id="in7"> rewrite equiv H.</span>
<span class="output-line" id="out7">[> Line 57: (rewrite equiv ...) <br>[goal> Focused goal (1/1):<br>System: left:default/left, right:default/left (same for equivalences)<br>Variables: i:index,tau,tau':timestamp<br>H: equiv(<span class="gm" style="font-weight: bold; color: #AA00AA">frame</span>@tau, diff(<span class="gm" style="font-weight: bold; color: #AA00AA">s</span>(i)@tau', <span class="gn" style="color: #AA5500">m</span>))<br>Hap: [<span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="gf" style="font-weight: bold">pred</span>(tau))]<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br><span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@tau <> <span class="gn" style="color: #AA5500">m</span><br><br></span>
<span class="com-line" id="com7"><p>Here, we use the <code>rewrite equiv</code> tactic to rewrite the conclusion of the goal: all occurrences of left elements from <code>H</code> are replaced by their corresponding right elements.</p>
<p>In this case, the tactic allows to replace <code>s(i)@tau'</code> by the name <code>m</code>.</p>
</span>
</span>
<span class="squirrel-step" id="step8">
<span class="input-line" id="in8"> intro H'.</span>
<span class="output-line" id="out8">[> Line 60: (intro H') <br>[goal> Focused goal (1/1):<br>System: left:default/left, right:default/left (same for equivalences)<br>Variables: i:index,tau,tau':timestamp<br>H: equiv(<span class="gm" style="font-weight: bold; color: #AA00AA">frame</span>@tau, diff(<span class="gm" style="font-weight: bold; color: #AA00AA">s</span>(i)@tau', <span class="gn" style="color: #AA5500">m</span>))<br>H': <span class="gm" style="font-weight: bold; color: #AA00AA">input</span>@tau = <span class="gn" style="color: #AA5500">m</span><br>Hap: [<span class="gm" style="font-weight: bold; color: #AA00AA">happens</span>(<span class="gf" style="font-weight: bold">pred</span>(tau))]<br><span class="sep" style="font-weight: bold">----------------------------------------</span><br>false<br><br></span>
<span class="com-line" id="com8"><p>It remains now to show that the attacker cannot deduce a fresh name, using the <code>fresh</code> tactic.</p>
</span>
</span>
<span class="squirrel-step" id="step9">
<span class="input-line" id="in9"> by fresh H'.</span>
<span class="output-line" id="out9">[> Line 60: by (fresh H') <br>[goal> Goal secrecy is proved <br></span>
</span>
<span class="squirrel-step" id="step10">
<span class="input-line" id="in10"><br>Qed.</span>
<span class="output-line" id="out10">Exiting proof mode.<br><br><br></span>
</span>
</span>
<div class="page-header">
<img src="logo-circular.png" class="logo">
<h1 class="project-tagline">Squirrel Prover</h1>
<a href="https://squirrel-prover.github.io/examples.html" class="header-button">
<button type="button" class="header-button">Exit</button>
</a>
<button type="button" class="header-button" onclick="help()" id="button-panel">Help</button>
</div>
<div class="help-panel" id="help-panel">
Press the left and right arrows to do and undo an instruction.
<br><br>
Alternatively, you can double-click on an instruction.
<br><br>
<span style="color: #8B0000;" onmouseenter="highlightOn('in-zone')" onmouseleave="highlightOff('in-zone')">This zone</span> shows a Squirrel file. You can double-click on a comment to collapse it for better readabilility.
<br><br>
<span style="color: #8B0000;" onmouseenter="highlightOn('out-zone')" onmouseleave="highlightOff('out-zone')">This zone</span> shows the output given by Squirrel.
<br><br>
<span style="color: #8B0000;" onmouseenter="highlightOn('prec-zone')" onmouseleave="highlightOff('prec-zone')">This zone</span> shows the output of the previous instruction, to help identifying the change caused by the instruction.
</div>
<div class="mainsection" id="main">
<div class="example-grid">
<div class="example-col example-col-left" id="in-zone">
<p class="example-code"><span id="in-line"></span></p>
</div>
<div class="example-col example-col-right">
<div class="example-code example-code-right" style="height: 45%; border-bottom: 4px double #8B0000;" id="prec-zone"><span>Previously:</span><br><br><span id="prec-line"></span>
</div>
<div style="position: relative;">
<button type="button" class="prec-button" onclick="hidePrec()" id="prec-button" >Hide</button>
</div>
<div class="example-code example-code-right" style="height: 55%;" id="out-zone"><span id="out-line"></span>
</div>
</div>
</div>
</div>
<script src="script.js"></script>
</body>