Skip to content

Commit 15e56ef

Browse files
dmzimmermandmzimmerman
committed
feat: composition of Internet-facing Tamarin subprotocols
1 parent 08bf830 commit 15e56ef

38 files changed

Lines changed: 3531 additions & 4645 deletions

File tree

‎models/cryptography/tamarin/Makefile‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -146,8 +146,8 @@ cv: clean subprotocols
146146
$(SPTHY) || exit 1;)
147147
@cat output/*.out | grep ProofScript | grep -v NoProofScript | grep -v verified | grep -v lemma > output/combined-proofscript-results.out || echo "RESULT: all proof scripts verified"
148148
@cat output/combined-proofscript-results.out
149-
@! [ -s output/combined-proofscript-results.out ]
150149
@grep falsified output/*.out || echo "RESULT: no lemmas falsified"
150+
@! [ -s output/combined-proofscript-results.out ]
151151
@ ! grep -q falsified output/*.out
152152

153153
# List of phony targets

‎models/cryptography/tamarin/compositions/README.md‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,4 +8,3 @@ The `make compositions` target of the parent directory [Makefile](../Makefile) b
88

99
- Bulletin Board Test - [bulletinboard_test.spthy.m4](./bulletinboard_test.spthy.m4): The composition of the bulletin board implementation and a protocol that exercises it, to "test" bulletin board properties
1010
- Internet Subprotocols - [internet_subprotocols.spthy.m4](./internet_subprotocols.spthy.m4): The composition of all subprotocols that are exposed to the Internet
11-
- Trustee Subprotocols - [trustee_subprotocols.spthy.m4](./trustee_subprotocols.spthy.m4): The composition of the trustee subprotocols after election key generation (i.e., mixing and decryption). The data generated by the other trustee subprotocols is used in these, but they do not run at the same time (election setup runs in isolation to ensure the trustees and TAS know all the trustee public keys and the election configuration; election key generation assumes that election setup is complete but doesn't necessarily happen at the same time).

‎models/cryptography/tamarin/compositions/includes/proofs/Sources_InternetProtocols.spthy.inc‎

Lines changed: 207 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,207 @@
1+
simplify
2+
solve( (∃ m1 m2 m3 m4 #i.
3+
(IN_SECURE_RECEIVE( m1, m2, m3, m4 ) @ #i)
4+
∧
5+
∀ #j. (SecureChannel_In( m1, m2, m3, m4 ) @ #j) ⇒ ¬(#j < #i)) ∥
6+
(∃ m1 m2 m3 m4 m5 m6 m7 #i.
7+
(IN_BALLOTCHECK_VA_CHECK( m1, m2, m3, m4, m5, m6, m7 ) @ #i)
8+
∧
9+
∀ #j.
10+
(OUT_BALLOTCHECK_VA_CHECK( m1, m2, m3, m4, m5, m6, m7 ) @ #j)
11+
⇒
12+
¬(#j < #i)) ∥
13+
(∃ m x #i.
14+
(IN_PSEUDO_TERM( m, x ) @ #i)
15+
∧
16+
(∀ #j. (!KU( x ) @ #j) ⇒ ¬(#j < #i)) ∧
17+
(∀ #j. (OUT_PSEUDO_TERM( m ) @ #j) ⇒ ¬(#j < #i))) )
18+
case case_1
19+
solve( IN_SECURE_RECEIVE( m1, m2, m3, m4 ) @ #i )
20+
case BallotCheck_DBB_ForwardRandomizers
21+
solve( DBB_State_ForwardRandomizers( ~ec, ~va_id, ~cid_va, ~bca_id,
22+
~cid_bca,
23+
<
24+
<'BCA_Check_Request', ~ec, tracker, pk_bca_encrypt,
25+
pk_bca_sign>,
26+
sig_bca_req>
27+
) ▶₀ #i )
28+
case BallotCheck_DBB_ReceiveCheckRequest
29+
solve( SecureReceive( ~cid_va, ~va_id, <~ec, 'DBB'>,
30+
<
31+
<'VA_Check_Randomizers',
32+
<
33+
<'BCA_Check_Request', ~ec,
34+
h(<
35+
<'BBEntry_Ballot_Submission', ~ec, timestamp,
36+
<'VA_Submit_Ballot', ~ec, pseudo, pk_voter, ~bs,
37+
ny_encrypt_c1(x, x.1, x.2), ny_encrypt_c2(x, x.1, x.2),
38+
ny_encrypt_p(x, x.1, x.2)>,
39+
sig>,
40+
ch>),
41+
pk_bca_encrypt, pk_bca_sign>,
42+
sig_bca_req>,
43+
encrypted_randomizers, pk_voter.1>,
44+
sig_randomizers>
45+
) ▶₁ #i )
46+
case SecureChannel_Receive_case_1
47+
by contradiction /* from formulas */
48+
next
49+
case SecureChannel_Receive_case_2
50+
by contradiction /* from formulas */
51+
qed
52+
qed
53+
next
54+
case BallotCheck_DBB_ReceiveCheckRequest
55+
solve( SecureReceive( ~cid_bca, ~bca_id, <~ec, 'DBB'>,
56+
<<'BCA_Check_Request', ~ec, tracker, pk_bca_encrypt, pk_bca_sign>,
57+
sig_bca_req>
58+
) ▶₃ #i )
59+
case SecureChannel_Receive_case_1
60+
by contradiction /* from formulas */
61+
next
62+
case SecureChannel_Receive_case_2
63+
by contradiction /* from formulas */
64+
qed
65+
next
66+
case BallotCheck_VA_RequestRandomizers
67+
solve( SecureReceive( ~cid, <~ec, 'DBB'>, ~va_id,
68+
<'DBB_Check_Request',
69+
<'BCA_Check_Request', ~ec, tracker, pk_bca_encrypt, pk_bca_sign>,
70+
sig_bca_req>
71+
) ▶₃ #i )
72+
case SecureChannel_Receive_case_1
73+
by contradiction /* from formulas */
74+
next
75+
case SecureChannel_Receive_case_2
76+
by contradiction /* from formulas */
77+
qed
78+
next
79+
case VoterAuthentication_AS_AuthenticationRequest
80+
solve( SecureReceive( ~cid, m2, 'AS',
81+
<'EAS_Request_Authentication_Session', ~project_id, ~api_key>
82+
) ▶₁ #i )
83+
case SecureChannel_Receive_case_1
84+
by contradiction /* from formulas */
85+
next
86+
case SecureChannel_Receive_case_2
87+
by contradiction /* from formulas */
88+
qed
89+
next
90+
case VoterAuthentication_AS_ReportAuthenticationResult
91+
solve( SecureReceive( ~cid, m2, 'AS',
92+
<'EAS_Request_Authentication_Result', ~session_id>
93+
) ▶₁ #i )
94+
case SecureChannel_Receive_case_1
95+
by contradiction /* from formulas */
96+
next
97+
case SecureChannel_Receive_case_2
98+
by contradiction /* from formulas */
99+
qed
100+
next
101+
case VoterAuthentication_AS_ReportIncompleteAuthenticationResult
102+
solve( SecureReceive( ~cid, m2, 'AS',
103+
<'EAS_Request_Authentication_Result', ~session_id>
104+
) ▶₁ #i )
105+
case SecureChannel_Receive_case_1
106+
by contradiction /* from formulas */
107+
next
108+
case SecureChannel_Receive_case_2
109+
by contradiction /* from formulas */
110+
qed
111+
next
112+
case VoterAuthentication_EAS_ReceiveAuthenticationComplete
113+
solve( SecureReceive( ~cid_va, ~va_id, <~ec, 'EAS'>,
114+
<'VA_Authentication_Complete', ~ec, pk_voter, ~token>
115+
) ▶₁ #i )
116+
case SecureChannel_Receive_case_1
117+
by contradiction /* from formulas */
118+
next
119+
case SecureChannel_Receive_case_2
120+
by contradiction /* from formulas */
121+
qed
122+
next
123+
case VoterAuthentication_EAS_RequestAuthentication
124+
solve( SecureReceive( ~cid_va, ~va_id, <~ec, 'EAS'>,
125+
<'VA_Request_Authentication', ~ec, pk_voter>
126+
) ▶₂ #i )
127+
case SecureChannel_Receive_case_1
128+
by contradiction /* from formulas */
129+
next
130+
case SecureChannel_Receive_case_2
131+
by contradiction /* from formulas */
132+
qed
133+
next
134+
case VoterAuthentication_VA_ReceiveAuthenticationResult_Eligible
135+
solve( SecureReceive( ~cid, <~ec, 'EAS'>, ~va_id,
136+
<'EAS_Authentication_Result', 'eligible', ~ec, pseudo,
137+
pk(~sk_voter), ballot_style>
138+
) ▶₁ #i )
139+
case SecureChannel_Receive_case_1
140+
by contradiction /* from formulas */
141+
next
142+
case SecureChannel_Receive_case_2
143+
by contradiction /* from formulas */
144+
qed
145+
qed
146+
next
147+
case case_2
148+
solve( VA_State_CheckOrCast( ~ec, ~va_id, $V, ~ballot, m5, ~r, m7
149+
) ▶₀ #i )
150+
case BallotCheck_VA_CheckResult_OK
151+
by contradiction /* from formulas */
152+
next
153+
case BallotSubmission_VA_BallotSubmitResponse_BallotTracker_Success
154+
by contradiction /* from formulas */
155+
qed
156+
next
157+
case case_3
158+
solve( !BB_Entry( ~bbid,
159+
<'BBEntry_Ballot_Submission', ~ec, timestamp,
160+
<'VA_Submit_Ballot', ~ec, x, pk(~sk_voter), ballot_style,
161+
cryptograms>,
162+
sign(<'VA_Submit_Ballot', ~ec, x, pk(~sk_voter), ballot_style,
163+
cryptograms>,
164+
'1', ~sk_voter)
165+
>,
166+
tracker, %idx
167+
) ▶₃ #i )
168+
case BulletinBoard_Append
169+
solve( SecureReceive( ~cid, <~ec, 'DBB'>, ~va_id,
170+
<'DBB_Ballot_Tracker', ~ec,
171+
h(<
172+
<'BBEntry_Ballot_Submission', ~ec, timestamp,
173+
<'VA_Submit_Ballot', ~ec, x, pk(~sk_voter), ballot_style,
174+
cryptograms>,
175+
sign(<'VA_Submit_Ballot', ~ec, x, pk(~sk_voter), ballot_style,
176+
cryptograms>,
177+
'1', ~sk_voter)
178+
>,
179+
ch>)
180+
>
181+
) ▶₄ #i )
182+
case SecureChannel_Receive_case_1
183+
by contradiction /* from formulas */
184+
next
185+
case SecureChannel_Receive_case_2
186+
by contradiction /* from formulas */
187+
next
188+
case SecureChannel_Receive_case_3
189+
solve( BB_Append_Request( ~bbid,
190+
<'BBEntry_Ballot_Submission', ~ec, timestamp,
191+
<'VA_Submit_Ballot', ~ec, x, pk(~sk_voter), ballot_style,
192+
cryptograms>,
193+
sign(<'VA_Submit_Ballot', ~ec, x, pk(~sk_voter), ballot_style,
194+
cryptograms>,
195+
'1', ~sk_voter)
196+
>,
197+
%idx
198+
)[+] ▶₂ #vr )
199+
case BallotSubmission_DBB_AppendSubmittedBallot_case_1
200+
by contradiction /* from formulas */
201+
next
202+
case BallotSubmission_DBB_AppendSubmittedBallot_case_2
203+
by contradiction /* from formulas */
204+
qed
205+
qed
206+
qed
207+
qed

‎models/cryptography/tamarin/compositions/internet_subprotocols.spthy.m4‎

Lines changed: 146 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -39,13 +39,35 @@ define(<!USE_UNIQUE!>)dnl
3939
define(<!USE_EUFCMA_SIGNING!>)dnl
4040
define(<!USE_ABSTRACTED_NAOR_YUNG!>)dnl
4141
define(<!USE_PSEUDONYM!>)dnl
42+
define(<!USE_EQUALITY!>)dnl
43+
define(<!USE_INEQUALITY!>)dnl
4244
include(common/primitives.m4.inc)
4345
define(<!USE_SECURE_CHANNELS!>)dnl
4446
define(<!USE_SECURE_CHANNELS_INJECTION!>)dnl
4547
define(<!USE_SECURE_CHANNELS_INTERCEPTION!>)dnl
4648
include(common/channels.m4.inc)
4749
define(<USE_NO_BB_ENTRY_FOR_HASH!>)dnl
4850
include(common/bulletinboard.m4.inc)
51+
define(<!USE_MOST_RECENT_AUTHORIZATION!>)dnl
52+
define(<!USE_UNAUTHORIZED!>)dnl
53+
define(<!USE_SUBMISSION_NOT_ON_BB!>)dnl
54+
define(<!USE_NO_PREVIOUS_CAST!>)dnl
55+
define(<!USE_MOST_RECENT_BALLOT!>)dnl
56+
include(common/ballot_restrictions.m4.inc)
57+
58+
/* Mock Election Setup */
59+
include(subprotocols/includes/mock_election_setup.m4.inc)
60+
61+
/*
62+
This rule has BB_Terminate_Request on its right-hand side, so
63+
that we don't get a well-formedness warning when we don't use it.
64+
Note that we are requesting to terminate a bulletin board that
65+
doesn't actually exist, so this has no real effect on anything.
66+
*/
67+
rule Mock_BBTerminate [role="Mock"]:
68+
[]
69+
--[ Unique('BallotSubmission_Mock_BB_Terminate') ]->
70+
[ BB_Terminate_Request('fake_bbid', %1) ]
4971

5072
/* Voter Authentication */
5173

@@ -63,5 +85,129 @@ include(subprotocols/ballot_cast.spthy.m4)
6385

6486
include(subprotocols/ballot_check.spthy.m4)
6587

88+
/* Sources */
89+
90+
/*
91+
This lemma says that incoming secure channel messages have
92+
to come from the secure channel rule, and that certain terms
93+
have to originate in certain rules. It is a translation of the
94+
lemma generated by Tamarin's "--auto-sources" option; however,
95+
it is _not_ marked as a sources lemma here because, when it is,
96+
Tamarin is unable to complete preprocessing regardless of how
97+
much memory it is given (up to 1 TB, at least).
98+
99+
It is, therefore, here primarily as a reminder to fix, and a
100+
starting point for fixing, the composed protocol's partial
101+
deconstructions in the future.
102+
*/
103+
define(<!PROOF_SCRIPT!>, ifdef(<!INCLUDE_PROOF_SCRIPTS!>, <!compositions/includes/proofs/Sources_InternetProtocols.spthy.inc!>, <!/tmp/NOPROOFSCRIPT!>))dnl
104+
syscmd(cat PROOF_SCRIPT > /dev/null 2>&1)dnl
105+
lemma ifelse(sysval, <!0!>, <!ProofScript!>, <!NoProofScript!>)_InternetProtocols_Sources /* [sources] */:
106+
"
107+
(
108+
All m1 m2 m3 m4 #i.
109+
IN_SECURE_RECEIVE(m1, m2, m3, m4)@i
110+
==>
111+
Ex #j.
112+
(
113+
SecureChannel_In(m1, m2, m3, m4)@j
114+
&
115+
#j < #i
116+
)
117+
)
118+
&
119+
(
120+
All m1 m2 m3 m4 m5 m6 m7 #i.
121+
IN_BALLOTCHECK_VA_CHECK(m1, m2, m3, m4, m5, m6, m7)@i
122+
==>
123+
Ex #j.
124+
(
125+
OUT_BALLOTCHECK_VA_CHECK(m1, m2, m3, m4, m5, m6, m7)@j
126+
&
127+
#j < #i
128+
)
129+
)
130+
&
131+
(
132+
All m x #i.
133+
IN_PSEUDO_TERM(m, x)@i
134+
==>
135+
(
136+
(Ex #j.
137+
(
138+
KU(x)@j
139+
&
140+
#j < #i
141+
)
142+
)
143+
|
144+
(Ex #j.
145+
(
146+
OUT_PSEUDO_TERM(m)@j
147+
&
148+
#j < #i
149+
)
150+
)
151+
)
152+
)
153+
"
154+
dnl Include the proof script, if one exists.
155+
sinclude(PROOF_SCRIPT)dnl
156+
157+
/* Composition Executability Lemmas */
158+
159+
/*
160+
Most of the executability lemmas from the individual protocols are
161+
too difficult for Tamarin to prove automatically even without the
162+
protocols being composed. What we really want to show for
163+
executability is that a ballot can be successfully cast, and a
164+
ballot can be successfully checked, by a voter that makes it all
165+
the way through the authentication, submission, and cast/check
166+
protocols. We eliminate the possibility of adversary action on the
167+
secure channels to reduce the search space.
168+
*/
169+
170+
/*
171+
This lemma states that a ballot can be successfully cast (and the
172+
VA receives confirmation of such).
173+
*/
174+
define(<!PROOF_SCRIPT!>, ifdef(<!INCLUDE_PROOF_SCRIPTS!>, <!compositions/includes/proofs/InternetProtocols_Cast_Confirm.spthy.inc!>, <!/tmp/NOPROOFSCRIPT!>))dnl
175+
syscmd(cat PROOF_SCRIPT > /dev/null 2>&1)dnl
176+
lemma ifelse(sysval, <!0!>, <!ProofScript!>, <!NoProofScript!>)_Executability_InternetProtocols_Cast_Confirm:
177+
exists-trace
178+
"
179+
(Ex ec va_id pseudo ballot cryptograms r sub_tracker cast_tracker #i.
180+
VA_CastConfirmation_Trace(ec, va_id, pseudo, ballot, cryptograms, r, sub_tracker, cast_tracker)@i)
181+
&
182+
/* prevent message injection to reduce search space */
183+
not (Ex m #t. SecureChannel_InjectedMessage(m)@t)
184+
&
185+
/* prevent message interception to reduce search space */
186+
not (Ex m #t. SecureChannel_InterceptedMessage(m)@t)
187+
"
188+
dnl Include the proof script, if one exists.
189+
sinclude(PROOF_SCRIPT)dnl
190+
191+
/*
192+
This lemma states that a ballot can be successfully checked (as evidenced
193+
by the VA being able to "OK" a ballot check).
194+
*/
195+
define(<!PROOF_SCRIPT!>, ifdef(<!INCLUDE_PROOF_SCRIPTS!>, <!compositions/includes/proofs/InternetProtocols_Check_OK.spthy.inc!>, <!/tmp/NOPROOFSCRIPT!>))dnl
196+
syscmd(cat PROOF_SCRIPT > /dev/null 2>&1)dnl
197+
lemma ifelse(sysval, <!0!>, <!ProofScript!>, <!NoProofScript!>)_Executability_InternetProtocols_Check_OK:
198+
exists-trace
199+
"
200+
(Ex ec va_id p b c r t pk #i.
201+
VA_CheckResult_OK_Trace(ec, va_id, p, b, c, r, t, pk)@i)
202+
&
203+
/* prevent message injection to reduce search space */
204+
not (Ex m #t. SecureChannel_InjectedMessage(m)@t)
205+
&
206+
/* prevent message interception to reduce search space */
207+
not (Ex m #t. SecureChannel_InterceptedMessage(m)@t)
208+
"
209+
dnl Include the proof script, if one exists.
210+
sinclude(PROOF_SCRIPT)dnl
211+
66212
dnl We don't need a newline here, it comes from the included file
67213
end

0 commit comments

Comments
 (0)