Public Git Hosting - rttp-proofs.git/search

2015-02-11	Tim Makarios	Proof that timely_delivery is continuously_satisfiable	commit \| commitdiff \| tree
2015-02-11	Tim Makarios	Defined events_before to simplify continuously_satisfiable	commit \| commitdiff \| tree
2015-02-10	Tim Makarios	Require doability for continuous satisfiability	commit \| commitdiff \| tree
2015-02-10	Tim Makarios	Defined the timely delivery protocol	commit \| commitdiff \| tree
2015-02-10	Tim Makarios	Changed a Signed message to a detached Signature for...	commit \| commitdiff \| tree
2015-02-04	Tim Makarios	Defined non_clairvoyant	commit \| commitdiff \| tree
2015-02-03	Tim Makarios	Defined apply_encrypted_message_map_event	commit \| commitdiff \| tree
2015-02-03	Tim Makarios	Defined apply_encrypted_message_map	commit \| commitdiff \| tree
2015-02-03	Tim Makarios	Require an indistinguishability_map to be a bijection	commit \| commitdiff \| tree
2015-01-23	Tim Makarios	Defined indistinguishability_map	commit \| commitdiff \| tree
2015-01-23	Tim Makarios	Definition of continuously_satisfiable	commit \| commitdiff \| tree
2015-01-23	Tim Makarios	Defined satisfied_protocol_at	commit \| commitdiff \| tree
2015-01-22	Tim Makarios	Defined possible_history	commit \| commitdiff \| tree
2015-01-22	Tim Makarios	Moved time and history to Communication.thy	commit \| commitdiff \| tree
2015-01-22	Tim Makarios	Lemma relating causal_agent and affected_agent	commit \| commitdiff \| tree
2015-01-22	Tim Makarios	Definition of affected_agent	commit \| commitdiff \| tree
2015-01-22	Tim Makarios	lemma relating doable and causal_agent	commit \| commitdiff \| tree
2015-01-22	Tim Makarios	Defined causal_agent for an event	commit \| commitdiff \| tree
2015-01-21	Tim Makarios	Reorganized Communication.thy for clarity	commit \| commitdiff \| tree
2015-01-21	Tim Makarios	Type synonyms for time, history, and protocol	commit \| commitdiff \| tree
2015-01-21	Tim Makarios	Definition of doable	commit \| commitdiff \| tree
2015-01-21	Tim Makarios	Explanatory comments about the definitions of learnable...	commit \| commitdiff \| tree
2015-01-21	Tim Makarios	Alter learnable and constructible to require minimal...	commit \| commitdiff \| tree
2015-01-20	Tim Makarios	Inductive definition of constructible messages	commit \| commitdiff \| tree
2015-01-20	Tim Makarios	Longer theorem names for inductive definition of learnable	commit \| commitdiff \| tree
2015-01-20	Tim Makarios	Inductive definition of learnable	commit \| commitdiff \| tree
2015-01-20	Tim Makarios	Simplify Pay event; time is whenever the event happens	commit \| commitdiff \| tree
2015-01-20	Tim Makarios	Type synonym actor, for clarity	commit \| commitdiff \| tree
2015-01-20	Tim Makarios	event datatype	commit \| commitdiff \| tree
2014-12-10	Tim Makarios	agent and message datatypes	commit \| commitdiff \| tree
2014-12-10	Tim Makarios	Communication layer theory	commit \| commitdiff \| tree
2014-12-10	Tim Makarios	Expand title of output pdf	commit \| commitdiff \| tree
2014-12-05	Tim Makarios	Trivial RTTP.thy	commit \| commitdiff \| tree
2014-12-05	Tim Makarios	Set author in root.tex	commit \| commitdiff \| tree
2014-12-05	Tim Makarios	isabelle mkroot -d	commit \| commitdiff \| tree

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

RSS Atom