-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathindex.html
69 lines (69 loc) · 15.9 KB
/
index.html
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
<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01//EN">
<html>
<head>
<title>ProVerif: main result page</title>
<link rel="stylesheet" href="cssproverif.css">
</head>
<body>
<H1>ProVerif results</H1>
<A HREF="eq.html">Equations & Destructors</A><br>
<A HREF="process_0.html" TARGET="process">Process</A><br>
<UL>
<LI><span class="query">Query event(<span class="fun">DecentAppGotMsg</span>(<span class="fun">enclaveE</span>,<span class="var">anyMsg</span>)) <span class="conn">==></span> <span class="var">anyMsg</span> <span class="conn">=</span> <span class="fun">legitimate_msg</span></span><br>
<A HREF="clauses1.html" TARGET="clauses">Clauses</A><br>
<A HREF="compclauses1.html">Completed clauses</A><br>
ok, secrecy assumption verified: fact unreachable <span class="pred">attacker</span>(<span class="fun">iasRepKeySeed</span>)<br>
ok, secrecy assumption verified: fact unreachable <span class="pred">attacker</span>(<span class="fun">encPrvsKeySeed</span>)<br>
ok, secrecy assumption verified: fact unreachable <span class="pred">attacker</span>(<span class="name">localRepKey</span>[!1 = <span class="var">v_727691</span>])<br>
ok, secrecy assumption verified: fact unreachable <span class="pred">attacker</span>(<span class="name">decentSvrKeySeed</span>[!2 = <span class="var">v_727689</span>,!1 = <span class="var">v_727690</span>])<br>
ok, secrecy assumption verified: fact unreachable <span class="pred">attacker</span>(<span class="name">enclaveRecvKeySeed</span>[someAuls1 = <span class="var">v_727686</span>,!2 = <span class="var">v_727687</span>,!1 = <span class="var">v_727688</span>])<br>
ok, secrecy assumption verified: fact unreachable <span class="pred">attacker</span>(<span class="name">enclaveVrfyEKeySeed</span>[!2 = <span class="var">v_727684</span>,!1 = <span class="var">v_727685</span>])<br>
ok, secrecy assumption verified: fact unreachable <span class="pred">attacker</span>(<span class="name">enclaveVrfyFKeySeed</span>[!2 = <span class="var">v_727682</span>,!1 = <span class="var">v_727683</span>])<br>
ok, secrecy assumption verified: fact unreachable <span class="pred">attacker</span>(<span class="name">enclaveVrfyE2KeySeed</span>[someAuls2 = <span class="var">v_727679</span>,!2 = <span class="var">v_727680</span>,!1 = <span class="var">v_727681</span>])<br>
ok, secrecy assumption verified: fact unreachable <span class="pred">attacker</span>(<span class="name">enclaveVrfyF2KeySeed</span>[someAuls3 = <span class="var">v_727676</span>,!2 = <span class="var">v_727677</span>,!1 = <span class="var">v_727678</span>])<br>
ok, secrecy assumption verified: fact unreachable <span class="pred">attacker</span>(<span class="name">enclaveEKeySeed</span>[!2 = <span class="var">v_727674</span>,!1 = <span class="var">v_727675</span>])<br>
ok, secrecy assumption verified: fact unreachable <span class="pred">attacker</span>(<span class="name">enclaveFKeySeed</span>[!2 = <span class="var">v_727672</span>,!1 = <span class="var">v_727673</span>])<br>
ok, secrecy assumption verified: fact unreachable <span class="pred">attacker</span>(<span class="fun">sskgen</span>(<span class="fun">iasRepKeySeed</span>))<br>
ok, secrecy assumption verified: fact unreachable <span class="pred">attacker</span>(<span class="fun">sskgen</span>(<span class="fun">encPrvsKeySeed</span>))<br>
ok, secrecy assumption verified: fact unreachable <span class="pred">attacker</span>(<span class="fun">sskgen</span>(<span class="name">localRepKey</span>[!1 = <span class="var">v_727671</span>]))<br>
ok, secrecy assumption verified: fact unreachable <span class="pred">attacker</span>(<span class="fun">sskgen</span>(<span class="name">decentSvrKeySeed</span>[!2 = <span class="var">v_727669</span>,!1 = <span class="var">v_727670</span>]))<br>
ok, secrecy assumption verified: fact unreachable <span class="pred">attacker</span>(<span class="fun">sskgen</span>(<span class="name">enclaveRecvKeySeed</span>[someAuls1 = <span class="var">v_727666</span>,!2 = <span class="var">v_727667</span>,!1 = <span class="var">v_727668</span>]))<br>
ok, secrecy assumption verified: fact unreachable <span class="pred">attacker</span>(<span class="fun">sskgen</span>(<span class="name">enclaveVrfyEKeySeed</span>[!2 = <span class="var">v_727664</span>,!1 = <span class="var">v_727665</span>]))<br>
ok, secrecy assumption verified: fact unreachable <span class="pred">attacker</span>(<span class="fun">sskgen</span>(<span class="name">enclaveVrfyFKeySeed</span>[!2 = <span class="var">v_727662</span>,!1 = <span class="var">v_727663</span>]))<br>
ok, secrecy assumption verified: fact unreachable <span class="pred">attacker</span>(<span class="fun">sskgen</span>(<span class="name">enclaveVrfyE2KeySeed</span>[someAuls2 = <span class="var">v_727659</span>,!2 = <span class="var">v_727660</span>,!1 = <span class="var">v_727661</span>]))<br>
ok, secrecy assumption verified: fact unreachable <span class="pred">attacker</span>(<span class="fun">sskgen</span>(<span class="name">enclaveVrfyF2KeySeed</span>[someAuls3 = <span class="var">v_727656</span>,!2 = <span class="var">v_727657</span>,!1 = <span class="var">v_727658</span>]))<br>
ok, secrecy assumption verified: fact unreachable <span class="pred">attacker</span>(<span class="fun">sskgen</span>(<span class="name">enclaveEKeySeed</span>[!2 = <span class="var">v_727654</span>,!1 = <span class="var">v_727655</span>]))<br>
ok, secrecy assumption verified: fact unreachable <span class="pred">attacker</span>(<span class="fun">sskgen</span>(<span class="name">enclaveFKeySeed</span>[!2 = <span class="var">v_727652</span>,!1 = <span class="var">v_727653</span>]))<br>
ok, secrecy assumption verified: fact unreachable <span class="pred">attacker</span>(<span class="name">decentSvrEcKey1</span>[!2 = <span class="var">v_727650</span>,!1 = <span class="var">v_727651</span>])<br>
ok, secrecy assumption verified: fact unreachable <span class="pred">attacker</span>(<span class="name">enclaveRecvEcKey1</span>[someAuls1 = <span class="var">v_727647</span>,!2 = <span class="var">v_727648</span>,!1 = <span class="var">v_727649</span>])<br>
ok, secrecy assumption verified: fact unreachable <span class="pred">attacker</span>(<span class="name">enclaveVrfyEEcKey1</span>[!2 = <span class="var">v_727645</span>,!1 = <span class="var">v_727646</span>])<br>
ok, secrecy assumption verified: fact unreachable <span class="pred">attacker</span>(<span class="name">enclaveVrfyFEcKey1</span>[!2 = <span class="var">v_727643</span>,!1 = <span class="var">v_727644</span>])<br>
ok, secrecy assumption verified: fact unreachable <span class="pred">attacker</span>(<span class="name">enclaveVrfyE2EcKey1</span>[someAuls2 = <span class="var">v_727640</span>,!2 = <span class="var">v_727641</span>,!1 = <span class="var">v_727642</span>])<br>
ok, secrecy assumption verified: fact unreachable <span class="pred">attacker</span>(<span class="name">enclaveVrfyF2EcKey1</span>[someAuls3 = <span class="var">v_727637</span>,!2 = <span class="var">v_727638</span>,!1 = <span class="var">v_727639</span>])<br>
ok, secrecy assumption verified: fact unreachable <span class="pred">attacker</span>(<span class="name">enclaveEEcKey1</span>[!2 = <span class="var">v_727635</span>,!1 = <span class="var">v_727636</span>])<br>
ok, secrecy assumption verified: fact unreachable <span class="pred">attacker</span>(<span class="name">enclaveEEcKey2</span>[!2 = <span class="var">v_727633</span>,!1 = <span class="var">v_727634</span>])<br>
ok, secrecy assumption verified: fact unreachable <span class="pred">attacker</span>(<span class="name">enclaveFEcKey1</span>[!2 = <span class="var">v_727631</span>,!1 = <span class="var">v_727632</span>])<br>
ok, secrecy assumption verified: fact unreachable <span class="pred">attacker</span>(<span class="name">enclaveFEcKey2</span>[!2 = <span class="var">v_727629</span>,!1 = <span class="var">v_727630</span>])<br>
ok, secrecy assumption verified: fact unreachable <span class="pred">attacker</span>(<span class="fun">EcDiHeToKey</span>(<span class="fun">DiHeExp</span>(<span class="fun">DiHeExp</span>(<span class="fun">DiHeValG</span>,<span class="name">enclaveEEcKey2</span>[!2 = <span class="var">v_727625</span>,!1 = <span class="var">v_727626</span>]),<span class="name">enclaveFEcKey2</span>[!2 = <span class="var">v_727627</span>,!1 = <span class="var">v_727628</span>])))<br>
ok, secrecy assumption verified: fact unreachable <span class="pred">attacker</span>(<span class="fun">EcDiHeToKey</span>(<span class="fun">DiHeExp</span>(<span class="fun">DiHeExp</span>(<span class="fun">DiHeValG</span>,<span class="name">enclaveFEcKey2</span>[!2 = <span class="var">v_727621</span>,!1 = <span class="var">v_727622</span>]),<span class="name">enclaveEEcKey2</span>[!2 = <span class="var">v_727623</span>,!1 = <span class="var">v_727624</span>])))<br>
ok, secrecy assumption verified: fact unreachable <span class="pred">attacker</span>(<span class="fun">EcDiHeToKey</span>(<span class="fun">DiHeExp</span>(<span class="fun">DiHeExp</span>(<span class="fun">DiHeValG</span>,<span class="name">decentSvrEcKey1</span>[!2 = <span class="var">v_727616</span>,!1 = <span class="var">v_727617</span>]),<span class="name">enclaveRecvEcKey1</span>[someAuls1 = <span class="var">v_727618</span>,!2 = <span class="var">v_727619</span>,!1 = <span class="var">v_727620</span>])))<br>
ok, secrecy assumption verified: fact unreachable <span class="pred">attacker</span>(<span class="fun">EcDiHeToKey</span>(<span class="fun">DiHeExp</span>(<span class="fun">DiHeExp</span>(<span class="fun">DiHeValG</span>,<span class="name">enclaveRecvEcKey1</span>[someAuls1 = <span class="var">v_727611</span>,!2 = <span class="var">v_727612</span>,!1 = <span class="var">v_727613</span>]),<span class="name">decentSvrEcKey1</span>[!2 = <span class="var">v_727614</span>,!1 = <span class="var">v_727615</span>])))<br>
ok, secrecy assumption verified: fact unreachable <span class="pred">attacker</span>(<span class="fun">EcDiHeToKey</span>(<span class="fun">DiHeExp</span>(<span class="fun">DiHeExp</span>(<span class="fun">DiHeValG</span>,<span class="name">decentSvrEcKey1</span>[!2 = <span class="var">v_727607</span>,!1 = <span class="var">v_727608</span>]),<span class="name">enclaveVrfyEEcKey1</span>[!2 = <span class="var">v_727609</span>,!1 = <span class="var">v_727610</span>])))<br>
ok, secrecy assumption verified: fact unreachable <span class="pred">attacker</span>(<span class="fun">EcDiHeToKey</span>(<span class="fun">DiHeExp</span>(<span class="fun">DiHeExp</span>(<span class="fun">DiHeValG</span>,<span class="name">enclaveVrfyEEcKey1</span>[!2 = <span class="var">v_727603</span>,!1 = <span class="var">v_727604</span>]),<span class="name">decentSvrEcKey1</span>[!2 = <span class="var">v_727605</span>,!1 = <span class="var">v_727606</span>])))<br>
ok, secrecy assumption verified: fact unreachable <span class="pred">attacker</span>(<span class="fun">EcDiHeToKey</span>(<span class="fun">DiHeExp</span>(<span class="fun">DiHeExp</span>(<span class="fun">DiHeValG</span>,<span class="name">decentSvrEcKey1</span>[!2 = <span class="var">v_727599</span>,!1 = <span class="var">v_727600</span>]),<span class="name">enclaveVrfyFEcKey1</span>[!2 = <span class="var">v_727601</span>,!1 = <span class="var">v_727602</span>])))<br>
ok, secrecy assumption verified: fact unreachable <span class="pred">attacker</span>(<span class="fun">EcDiHeToKey</span>(<span class="fun">DiHeExp</span>(<span class="fun">DiHeExp</span>(<span class="fun">DiHeValG</span>,<span class="name">enclaveVrfyFEcKey1</span>[!2 = <span class="var">v_727595</span>,!1 = <span class="var">v_727596</span>]),<span class="name">decentSvrEcKey1</span>[!2 = <span class="var">v_727597</span>,!1 = <span class="var">v_727598</span>])))<br>
ok, secrecy assumption verified: fact unreachable <span class="pred">attacker</span>(<span class="fun">EcDiHeToKey</span>(<span class="fun">DiHeExp</span>(<span class="fun">DiHeExp</span>(<span class="fun">DiHeValG</span>,<span class="name">decentSvrEcKey1</span>[!2 = <span class="var">v_727590</span>,!1 = <span class="var">v_727591</span>]),<span class="name">enclaveVrfyE2EcKey1</span>[someAuls2 = <span class="var">v_727592</span>,!2 = <span class="var">v_727593</span>,!1 = <span class="var">v_727594</span>])))<br>
ok, secrecy assumption verified: fact unreachable <span class="pred">attacker</span>(<span class="fun">EcDiHeToKey</span>(<span class="fun">DiHeExp</span>(<span class="fun">DiHeExp</span>(<span class="fun">DiHeValG</span>,<span class="name">enclaveVrfyE2EcKey1</span>[someAuls2 = <span class="var">v_727585</span>,!2 = <span class="var">v_727586</span>,!1 = <span class="var">v_727587</span>]),<span class="name">decentSvrEcKey1</span>[!2 = <span class="var">v_727588</span>,!1 = <span class="var">v_727589</span>])))<br>
ok, secrecy assumption verified: fact unreachable <span class="pred">attacker</span>(<span class="fun">EcDiHeToKey</span>(<span class="fun">DiHeExp</span>(<span class="fun">DiHeExp</span>(<span class="fun">DiHeValG</span>,<span class="name">decentSvrEcKey1</span>[!2 = <span class="var">v_727580</span>,!1 = <span class="var">v_727581</span>]),<span class="name">enclaveVrfyF2EcKey1</span>[someAuls3 = <span class="var">v_727582</span>,!2 = <span class="var">v_727583</span>,!1 = <span class="var">v_727584</span>])))<br>
ok, secrecy assumption verified: fact unreachable <span class="pred">attacker</span>(<span class="fun">EcDiHeToKey</span>(<span class="fun">DiHeExp</span>(<span class="fun">DiHeExp</span>(<span class="fun">DiHeValG</span>,<span class="name">enclaveVrfyF2EcKey1</span>[someAuls3 = <span class="var">v_727575</span>,!2 = <span class="var">v_727576</span>,!1 = <span class="var">v_727577</span>]),<span class="name">decentSvrEcKey1</span>[!2 = <span class="var">v_727578</span>,!1 = <span class="var">v_727579</span>])))<br>
ok, secrecy assumption verified: fact unreachable <span class="pred">attacker</span>(<span class="fun">EcDiHeToKey</span>(<span class="fun">DiHeExp</span>(<span class="fun">DiHeExp</span>(<span class="fun">DiHeValG</span>,<span class="name">decentSvrEcKey1</span>[!2 = <span class="var">v_727571</span>,!1 = <span class="var">v_727572</span>]),<span class="name">enclaveEEcKey1</span>[!2 = <span class="var">v_727573</span>,!1 = <span class="var">v_727574</span>])))<br>
ok, secrecy assumption verified: fact unreachable <span class="pred">attacker</span>(<span class="fun">EcDiHeToKey</span>(<span class="fun">DiHeExp</span>(<span class="fun">DiHeExp</span>(<span class="fun">DiHeValG</span>,<span class="name">enclaveEEcKey1</span>[!2 = <span class="var">v_727567</span>,!1 = <span class="var">v_727568</span>]),<span class="name">decentSvrEcKey1</span>[!2 = <span class="var">v_727569</span>,!1 = <span class="var">v_727570</span>])))<br>
ok, secrecy assumption verified: fact unreachable <span class="pred">attacker</span>(<span class="fun">EcDiHeToKey</span>(<span class="fun">DiHeExp</span>(<span class="fun">DiHeExp</span>(<span class="fun">DiHeValG</span>,<span class="name">decentSvrEcKey1</span>[!2 = <span class="var">v_727563</span>,!1 = <span class="var">v_727564</span>]),<span class="name">enclaveFEcKey1</span>[!2 = <span class="var">v_727565</span>,!1 = <span class="var">v_727566</span>])))<br>
ok, secrecy assumption verified: fact unreachable <span class="pred">attacker</span>(<span class="fun">EcDiHeToKey</span>(<span class="fun">DiHeExp</span>(<span class="fun">DiHeExp</span>(<span class="fun">DiHeValG</span>,<span class="name">enclaveFEcKey1</span>[!2 = <span class="var">v_727559</span>,!1 = <span class="var">v_727560</span>]),<span class="name">decentSvrEcKey1</span>[!2 = <span class="var">v_727561</span>,!1 = <span class="var">v_727562</span>])))<br>
<UL>
<LI>goal reachable: <span class="pred">end</span>(<span class="fun">DecentAppGotMsg</span>(<span class="fun">enclaveE</span>,<span class="fun">legitimate_msg</span>))<br>
</UL>
<span class="result">RESULT event(<span class="fun">DecentAppGotMsg</span>(<span class="fun">enclaveE</span>,<span class="var">anyMsg</span>)) <span class="conn">==></span> <span class="var">anyMsg</span> <span class="conn">=</span> <span class="fun">legitimate_msg</span> is <span class="trueresult">true</span>.</span><br>
</UL>
</body>
</html>