github.com/katzenpost/formal_specifications commits

client2: improve TLA+ specification

f0e637476b4867a85c28517a90b7059d1a03426f authored 11 months ago

client2: promela WIP from this morning

05eeb4db5f74dce3e727a4884e82e1de7e2b8a76 authored 11 months ago

client2: more improvements to the tla+ spec

1a9e06c6ac3d817c83e240984949deba0405b435 authored 11 months ago

client2: improve tla+ spec

9717ff4be09336d623535dd1a9a4532b218873f9 authored 11 months ago

WIP Update client2 promela spec

aed83291f0d7b878bdd438c5fa68f6af72875261 authored 11 months ago

try to fix client2 tla spec

8ae23a15808578e29f541643931fc22731f0112a authored 11 months ago

client2.pml WIP

c158d99cd9b5a202c79c66a301094477edd88b15 authored 11 months ago

Fix rwmutex promela model

b879ef7bfda834fa7246d29fb3ad33cac5a24f7c authored 12 months ago

Add promela model of rwmutex and waitgroup

bc36ef3833a7a92c04a0a3fcb9d27943c0930a2f authored 12 months ago

client2: move tla+ spec to subdir

fc84d89a6727480719d05832236430afb976158e authored 12 months ago

client2 WIP

bfa9824da506dfc872be5816effaa41b7a22ce6c authored 12 months ago

rm old client tla+ spec, and new client2 partial spec

6066608726041c21d43097d737f7eca493fc4416 authored 12 months ago

Add dirauth fsm spec, wip

833c8f80c1e9d2468c755c4c3eae971be64d0482 authored over 1 year ago

wip

041c1d9674086361f74472c9d349999fdf14ace0 authored over 1 year ago

more kem sphinx wip

bf0ad66a09f9ab0d3f5404908beb2833a81d4249 authored over 1 year ago

proverif kem sphinx work in progress

508ed4d747c6660333f1aa960e0e365a3c0b5434 authored over 1 year ago

KEM Sphinx ProVerif Specification: add more corrections

cd3bd0aa4228a79be5181152900ff74831a71420 authored over 1 year ago

kem_sphinx.passive.pv: try to debug it and fix it

414e7cdf8ce9734899a1b0a634f5f7c5612d7013 authored over 1 year ago

Add super rough draft KEM Sphinx ProVerif spec!

3b548d79230f764920b0edc7e9bd1e5633758880 authored over 1 year ago

Update both kem sphinx models

4e3bd80ce0f30a849ec98b9bb1bcd5a89fafacb0 authored over 1 year ago

rename to active and passive models

3b3fe17a4566d22f00ad008ab9b34aa9fcfc9d66 authored over 1 year ago

simplify kem sphinx model

91a161a01edd28837d42e68ad9bcdcef0d1434dc authored over 1 year ago

kem sphinx vp: check checkable primitives

4fdae20a4bec784ae42f034984e4143a37aff6ab authored over 1 year ago

add more nominal improvements to the kem sphinx spec

dc94d6959581cd0a031706b5806248c87aba7e62 authored over 1 year ago

sphinx.vp rename mix priv keys

6b1b8310c2737fed215743ee98844296924c8cbf authored over 1 year ago

try to fix the kem sphinx spec

fc31ea7312ffcbe180ade60c94f6c0c18c176e01 authored over 1 year ago

Add basic kem sphinx model, wip

e3f9417280ef8374c7dff0b8ed28ae544e6bde54 authored over 1 year ago

sphinx.vp: attempt to fix verification by making the model smaller

88f46a9707c0da3b52dd83fc17e5be303e88c704 authored over 1 year ago

attempt to fix sphinx model

0547c835609ebf39c36962591b960e25e2d7f1f4 authored over 1 year ago

Add verifpal spec for Sphinx

67618cb646465866ccab1fbb58eba4cf7d0f3764 authored over 1 year ago

Fix TLA+ dirauth protocol model

7570886e69b43356ce3354999f0da6e0dce99889 authored over 1 year ago

dirauth high level protocol TLA+ model work in progress

7c7c0d7906fe5be759ba25e7c2a65cc2974cf781 authored over 1 year ago

break up client fsm into many actions

3c624fbca3d484a1f84e6d8b7c719619ff8e18d0 authored over 1 year ago

Merge branch 'client2'

732de50751fd56a4b8d885e5d2fe8c1998798e64 authored over 1 year ago

Add noise XX proverif specs

ffd7c2f6c09c3e2ce56d0d032aa58b60c782af34 authored over 1 year ago

change attacker to passive

6ed33191b476a47f14f2440ccb21a6d1bca44629 authored over 1 year ago

wip

99799fa0d394d3cd7f4d2093a67eb8b0d0ca9b1d authored over 1 year ago

WIP

bdb6d15c9fe9b30f7f9ce8fdf8267e6152e03b3e authored over 1 year ago

Add super basic chat protocol

eeb88be248dc52fc8d82e9b37261d5150450c349 authored over 1 year ago

wip

f2f4920a71517eab9daad627f8123c3097b3a944 authored over 1 year ago

WIP

64ce38974e2e5e2cb8ef0bc5663d15e5044a75e2 authored over 1 year ago

Initial commit

2bbab65230f7e6954da7c4467bd9aefd089753cf authored over 1 year ago

Ecosyste.ms: OpenCollective

github.com/katzenpost/formal_specifications