Public Git Hosting - rttp-proofs.git/summary

description	This is intended to be a computer-verifiable (but somewhat human-readable) collection of proofs that RTTP has certain properties.
owner	tjm1983@gmail.com
last change	Fri, 19 Jun 2015 00:55:55 +0000 (19 12:55 +1200)
URL	git://repo.or.cz/rttp-proofs.git
	https://repo.or.cz/rttp-proofs.git
push URL	ssh://repo.or.cz/rttp-proofs.git
	https://repo.or.cz/rttp-proofs.git ^{(learn more)}
bundle info	rttp-proofs.git downloadable bundles
content tags add:	isabelle proof rttp transactions traversal trust

readme

RTTP is an in-development protocol for coordinating payments through trust networks. RTTP might stand for Responsible Trust Traversal Protocol or maybe Responsible Traversal Transaction Protocol, but probably not Responsible Transitive Transactions Protocol, and definitely not Real-time Transport Protocol, which should probably be just RTP.

2015-06-19	Tim Makarios	Proved constructed_from_not_received_implies_constructedmaster	commit \| commitdiff \| tree \| snapshot (tar.gz zip)
2015-06-17	Tim Makarios	Proved list_constructed_from	commit \| commitdiff \| tree \| snapshot (tar.gz zip)
2015-06-17	Tim Makarios	Proved encrypted_constructed_from	commit \| commitdiff \| tree \| snapshot (tar.gz zip)
2015-06-17	Tim Makarios	Proved that "events_not_after h t" is monotonic in t	commit \| commitdiff \| tree \| snapshot (tar.gz zip)
2015-06-16	Tim Makarios	Proved that "events_before h t" is monotonic in t	commit \| commitdiff \| tree \| snapshot (tar.gz zip)
2015-06-12	Tim Makarios	Proved that constructed_from is transitive	commit \| commitdiff \| tree \| snapshot (tar.gz zip)
2015-06-11	Tim Makarios	Prove a lemma characterizing events_not_after	commit \| commitdiff \| tree \| snapshot (tar.gz zip)
2015-06-11	Tim Makarios	Proved signature_constructed_from	commit \| commitdiff \| tree \| snapshot (tar.gz zip)
2015-05-08	Tim Makarios	Named constructed_from cases	commit \| commitdiff \| tree \| snapshot (tar.gz zip)
2015-05-08	Tim Makarios	Proved that a Number is constructed_from only itself	commit \| commitdiff \| tree \| snapshot (tar.gz zip)
2015-05-08	Tim Makarios	Proved that an ActorName is constructed_from only itself	commit \| commitdiff \| tree \| snapshot (tar.gz zip)
2015-05-08	Tim Makarios	Defined events_not_after	commit \| commitdiff \| tree \| snapshot (tar.gz zip)
2015-05-07	Tim Makarios	Proved learnable_implies_constructed_from	commit \| commitdiff \| tree \| snapshot (tar.gz zip)
2015-05-07	Tim Makarios	Defined constructed_from	commit \| commitdiff \| tree \| snapshot (tar.gz zip)
2015-05-07	Tim Makarios	An actor can construct anything learnable from anythi...	commit \| commitdiff \| tree \| snapshot (tar.gz zip)
2015-05-07	Tim Makarios	Redefined rttp_promises using Construct instead of...	commit \| commitdiff \| tree \| snapshot (tar.gz zip)
...

9 years ago

master

log | tree

This is intended to be a computer-verifiable (but somewhat human-readable) collection of proofs that RTTP has certain properties.

RSS Atom