Ecosyste.ms: OpenCollective
An open API service for software projects hosted on Open Collective.
github.com/katzenpost/formal_specifications
formal specifications
https://github.com/katzenpost/formal_specifications
client2: improve TLA+ specification
f0e637476b4867a85c28517a90b7059d1a03426f authored 10 months ago by David Stainton <[email protected]>
f0e637476b4867a85c28517a90b7059d1a03426f authored 10 months ago by David Stainton <[email protected]>
client2: promela WIP from this morning
05eeb4db5f74dce3e727a4884e82e1de7e2b8a76 authored 10 months ago by David Stainton <[email protected]>
05eeb4db5f74dce3e727a4884e82e1de7e2b8a76 authored 10 months ago by David Stainton <[email protected]>
client2: more improvements to the tla+ spec
1a9e06c6ac3d817c83e240984949deba0405b435 authored 10 months ago by David Stainton <[email protected]>
1a9e06c6ac3d817c83e240984949deba0405b435 authored 10 months ago by David Stainton <[email protected]>
client2: improve tla+ spec
9717ff4be09336d623535dd1a9a4532b218873f9 authored 10 months ago by David Stainton <[email protected]>
9717ff4be09336d623535dd1a9a4532b218873f9 authored 10 months ago by David Stainton <[email protected]>
WIP Update client2 promela spec
aed83291f0d7b878bdd438c5fa68f6af72875261 authored 10 months ago by David Stainton <[email protected]>
aed83291f0d7b878bdd438c5fa68f6af72875261 authored 10 months ago by David Stainton <[email protected]>
try to fix client2 tla spec
8ae23a15808578e29f541643931fc22731f0112a authored 10 months ago by David Stainton <[email protected]>
8ae23a15808578e29f541643931fc22731f0112a authored 10 months ago by David Stainton <[email protected]>
client2.pml WIP
c158d99cd9b5a202c79c66a301094477edd88b15 authored 10 months ago by David Stainton <[email protected]>
c158d99cd9b5a202c79c66a301094477edd88b15 authored 10 months ago by David Stainton <[email protected]>
Fix rwmutex promela model
b879ef7bfda834fa7246d29fb3ad33cac5a24f7c authored 10 months ago by David Stainton <[email protected]>
b879ef7bfda834fa7246d29fb3ad33cac5a24f7c authored 10 months ago by David Stainton <[email protected]>
Add promela model of rwmutex and waitgroup
bc36ef3833a7a92c04a0a3fcb9d27943c0930a2f authored 11 months ago by David Stainton <[email protected]>
bc36ef3833a7a92c04a0a3fcb9d27943c0930a2f authored 11 months ago by David Stainton <[email protected]>
client2: move tla+ spec to subdir
fc84d89a6727480719d05832236430afb976158e authored 11 months ago by David Stainton <[email protected]>
fc84d89a6727480719d05832236430afb976158e authored 11 months ago by David Stainton <[email protected]>
client2 WIP
bfa9824da506dfc872be5816effaa41b7a22ce6c authored 11 months ago by David Stainton <[email protected]>
bfa9824da506dfc872be5816effaa41b7a22ce6c authored 11 months ago by David Stainton <[email protected]>
rm old client tla+ spec, and new client2 partial spec
6066608726041c21d43097d737f7eca493fc4416 authored 11 months ago by David Stainton <[email protected]>
6066608726041c21d43097d737f7eca493fc4416 authored 11 months ago by David Stainton <[email protected]>
Add dirauth fsm spec, wip
833c8f80c1e9d2468c755c4c3eae971be64d0482 authored over 1 year ago by David Stainton <[email protected]>
833c8f80c1e9d2468c755c4c3eae971be64d0482 authored over 1 year ago by David Stainton <[email protected]>
wip
041c1d9674086361f74472c9d349999fdf14ace0 authored over 1 year ago by David Stainton <[email protected]>
041c1d9674086361f74472c9d349999fdf14ace0 authored over 1 year ago by David Stainton <[email protected]>
more kem sphinx wip
bf0ad66a09f9ab0d3f5404908beb2833a81d4249 authored over 1 year ago by David Stainton <[email protected]>
bf0ad66a09f9ab0d3f5404908beb2833a81d4249 authored over 1 year ago by David Stainton <[email protected]>
proverif kem sphinx work in progress
508ed4d747c6660333f1aa960e0e365a3c0b5434 authored over 1 year ago by David Stainton <[email protected]>
508ed4d747c6660333f1aa960e0e365a3c0b5434 authored over 1 year ago by David Stainton <[email protected]>
KEM Sphinx ProVerif Specification: add more corrections
cd3bd0aa4228a79be5181152900ff74831a71420 authored over 1 year ago by David Stainton <[email protected]>
cd3bd0aa4228a79be5181152900ff74831a71420 authored over 1 year ago by David Stainton <[email protected]>
kem_sphinx.passive.pv: try to debug it and fix it
414e7cdf8ce9734899a1b0a634f5f7c5612d7013 authored over 1 year ago by David Stainton <[email protected]>
414e7cdf8ce9734899a1b0a634f5f7c5612d7013 authored over 1 year ago by David Stainton <[email protected]>
Add super rough draft KEM Sphinx ProVerif spec!
3b548d79230f764920b0edc7e9bd1e5633758880 authored over 1 year ago by David Stainton <[email protected]>
3b548d79230f764920b0edc7e9bd1e5633758880 authored over 1 year ago by David Stainton <[email protected]>
Update both kem sphinx models
4e3bd80ce0f30a849ec98b9bb1bcd5a89fafacb0 authored over 1 year ago by David Stainton <[email protected]>
4e3bd80ce0f30a849ec98b9bb1bcd5a89fafacb0 authored over 1 year ago by David Stainton <[email protected]>
rename to active and passive models
3b3fe17a4566d22f00ad008ab9b34aa9fcfc9d66 authored over 1 year ago by David Stainton <[email protected]>
3b3fe17a4566d22f00ad008ab9b34aa9fcfc9d66 authored over 1 year ago by David Stainton <[email protected]>
simplify kem sphinx model
91a161a01edd28837d42e68ad9bcdcef0d1434dc authored over 1 year ago by David Stainton <[email protected]>
91a161a01edd28837d42e68ad9bcdcef0d1434dc authored over 1 year ago by David Stainton <[email protected]>
kem sphinx vp: check checkable primitives
4fdae20a4bec784ae42f034984e4143a37aff6ab authored over 1 year ago by David Stainton <[email protected]>
4fdae20a4bec784ae42f034984e4143a37aff6ab authored over 1 year ago by David Stainton <[email protected]>
add more nominal improvements to the kem sphinx spec
dc94d6959581cd0a031706b5806248c87aba7e62 authored over 1 year ago by David Stainton <[email protected]>
dc94d6959581cd0a031706b5806248c87aba7e62 authored over 1 year ago by David Stainton <[email protected]>
sphinx.vp rename mix priv keys
6b1b8310c2737fed215743ee98844296924c8cbf authored over 1 year ago by David Stainton <[email protected]>
6b1b8310c2737fed215743ee98844296924c8cbf authored over 1 year ago by David Stainton <[email protected]>
try to fix the kem sphinx spec
fc31ea7312ffcbe180ade60c94f6c0c18c176e01 authored over 1 year ago by David Stainton <[email protected]>
fc31ea7312ffcbe180ade60c94f6c0c18c176e01 authored over 1 year ago by David Stainton <[email protected]>
Add basic kem sphinx model, wip
e3f9417280ef8374c7dff0b8ed28ae544e6bde54 authored over 1 year ago by David Stainton <[email protected]>
e3f9417280ef8374c7dff0b8ed28ae544e6bde54 authored over 1 year ago by David Stainton <[email protected]>
sphinx.vp: attempt to fix verification by making the model smaller
88f46a9707c0da3b52dd83fc17e5be303e88c704 authored over 1 year ago by David Stainton <[email protected]>
88f46a9707c0da3b52dd83fc17e5be303e88c704 authored over 1 year ago by David Stainton <[email protected]>
attempt to fix sphinx model
0547c835609ebf39c36962591b960e25e2d7f1f4 authored over 1 year ago by David Stainton <[email protected]>
0547c835609ebf39c36962591b960e25e2d7f1f4 authored over 1 year ago by David Stainton <[email protected]>
Add verifpal spec for Sphinx
67618cb646465866ccab1fbb58eba4cf7d0f3764 authored over 1 year ago by David Stainton <[email protected]>
67618cb646465866ccab1fbb58eba4cf7d0f3764 authored over 1 year ago by David Stainton <[email protected]>
Fix TLA+ dirauth protocol model
7570886e69b43356ce3354999f0da6e0dce99889 authored over 1 year ago by David Stainton <[email protected]>
7570886e69b43356ce3354999f0da6e0dce99889 authored over 1 year ago by David Stainton <[email protected]>
dirauth high level protocol TLA+ model work in progress
7c7c0d7906fe5be759ba25e7c2a65cc2974cf781 authored over 1 year ago by David Stainton <[email protected]>
7c7c0d7906fe5be759ba25e7c2a65cc2974cf781 authored over 1 year ago by David Stainton <[email protected]>
break up client fsm into many actions
3c624fbca3d484a1f84e6d8b7c719619ff8e18d0 authored over 1 year ago by David Stainton <[email protected]>
3c624fbca3d484a1f84e6d8b7c719619ff8e18d0 authored over 1 year ago by David Stainton <[email protected]>
Merge branch 'client2'
732de50751fd56a4b8d885e5d2fe8c1998798e64 authored over 1 year ago by David Stainton <[email protected]>
732de50751fd56a4b8d885e5d2fe8c1998798e64 authored over 1 year ago by David Stainton <[email protected]>
Add noise XX proverif specs
ffd7c2f6c09c3e2ce56d0d032aa58b60c782af34 authored over 1 year ago by David Stainton <[email protected]>
ffd7c2f6c09c3e2ce56d0d032aa58b60c782af34 authored over 1 year ago by David Stainton <[email protected]>
change attacker to passive
6ed33191b476a47f14f2440ccb21a6d1bca44629 authored over 1 year ago by David Stainton <[email protected]>
6ed33191b476a47f14f2440ccb21a6d1bca44629 authored over 1 year ago by David Stainton <[email protected]>
wip
99799fa0d394d3cd7f4d2093a67eb8b0d0ca9b1d authored over 1 year ago by David Stainton <[email protected]>
99799fa0d394d3cd7f4d2093a67eb8b0d0ca9b1d authored over 1 year ago by David Stainton <[email protected]>
WIP
bdb6d15c9fe9b30f7f9ce8fdf8267e6152e03b3e authored over 1 year ago by David Stainton <[email protected]>
bdb6d15c9fe9b30f7f9ce8fdf8267e6152e03b3e authored over 1 year ago by David Stainton <[email protected]>
Add super basic chat protocol
eeb88be248dc52fc8d82e9b37261d5150450c349 authored over 1 year ago by David Stainton <[email protected]>
eeb88be248dc52fc8d82e9b37261d5150450c349 authored over 1 year ago by David Stainton <[email protected]>
wip
f2f4920a71517eab9daad627f8123c3097b3a944 authored over 1 year ago by David Stainton <[email protected]>
f2f4920a71517eab9daad627f8123c3097b3a944 authored over 1 year ago by David Stainton <[email protected]>
WIP
64ce38974e2e5e2cb8ef0bc5663d15e5044a75e2 authored over 1 year ago by David Stainton <[email protected]>
64ce38974e2e5e2cb8ef0bc5663d15e5044a75e2 authored over 1 year ago by David Stainton <[email protected]>
Initial commit
2bbab65230f7e6954da7c4467bd9aefd089753cf authored over 1 year ago by David Stainton <[email protected]>
2bbab65230f7e6954da7c4467bd9aefd089753cf authored over 1 year ago by David Stainton <[email protected]>