Public Git Hosting - rttp-proofs.git/search

2015-05-08	Tim Makarios	Named constructed_from cases	commit \| commitdiff \| tree
2015-05-08	Tim Makarios	Proved that a Number is constructed_from only itself	commit \| commitdiff \| tree
2015-05-08	Tim Makarios	Proved that an ActorName is constructed_from only itself	commit \| commitdiff \| tree
2015-05-08	Tim Makarios	Defined events_not_after	commit \| commitdiff \| tree
2015-05-07	Tim Makarios	Proved learnable_implies_constructed_from	commit \| commitdiff \| tree
2015-05-07	Tim Makarios	Defined constructed_from	commit \| commitdiff \| tree
2015-05-07	Tim Makarios	An actor can construct anything learnable from anything...	commit \| commitdiff \| tree
2015-05-07	Tim Makarios	Redefined rttp_promises using Construct instead of...	commit \| commitdiff \| tree
2015-05-06	Tim Makarios	Updated Protocols.thy to work with the new definition...	commit \| commitdiff \| tree
2015-05-05	Tim Makarios	Introduced Construct as an intermediate event, prior...	commit \| commitdiff \| tree
2015-05-01	Tim Makarios	Split sendable'_imples_sendable from proof of self_encryptio...	commit \| commitdiff \| tree
2015-04-30	Tim Makarios	Defined rttp_promises protocol	commit \| commitdiff \| tree
2015-04-30	Tim Makarios	Type synonym payment, for clarity	commit \| commitdiff \| tree
2015-04-30	Tim Makarios	Defined complete_agreement	commit \| commitdiff \| tree
2015-04-30	Tim Makarios	Defined signatures_for_complete_agreement	commit \| commitdiff \| tree
2015-04-15	Tim Makarios	Proved that the self_encryption protocol is non_clairvoyant	commit \| commitdiff \| tree
2015-04-14	Tim Makarios	Corrected definition of self_encryption protocol	commit \| commitdiff \| tree
2015-04-08	Tim Makarios	Proved that the inverse of an indistinguishability_map...	commit \| commitdiff \| tree
2015-04-02	Tim Makarios	Showed "map f (map (inv f) xs) = xs" if "bij f" is...	commit \| commitdiff \| tree
2015-04-02	Tim Makarios	Header for Miscellany.thy	commit \| commitdiff \| tree
2015-04-02	Tim Makarios	Showed "inv f y = x" is equivalent to "f x = y" if...	commit \| commitdiff \| tree
2015-04-02	Tim Makarios	Added "f (inv f x) = x" (when "bij f") as a simplification...	commit \| commitdiff \| tree
2015-03-25	Tim Makarios	Messages indistinguishable to an Actor are of the same...	commit \| commitdiff \| tree
2015-03-25	Tim Makarios	Types of messages	commit \| commitdiff \| tree
2015-03-06	Tim Makarios	ISC Licence	commit \| commitdiff \| tree
2015-03-05	Tim Makarios	Removed old indistinguishability_map and non_clairvoyant	commit \| commitdiff \| tree
2015-03-05	Tim Makarios	Proved alternative timely_delivery_non_clairvoyant	commit \| commitdiff \| tree
2015-03-04	Tim Makarios	Proved alternative Meet_non_clairvoyant	commit \| commitdiff \| tree
2015-03-03	Tim Makarios	Defined alternative non_clairvoyant	commit \| commitdiff \| tree
2015-03-03	Tim Makarios	Defined messages_received_before	commit \| commitdiff \| tree
2015-03-03	Tim Makarios	Ignore copies autosaved by jEdit	commit \| commitdiff \| tree
2015-03-03	Tim Makarios	Defined messages_received	commit \| commitdiff \| tree
2015-02-27	Tim Makarios	Defined lift_message_map_event	commit \| commitdiff \| tree
2015-02-20	Tim Makarios	Proof that indistinguishability_maps preserve learnability	commit \| commitdiff \| tree
2015-02-20	Tim Makarios	Proof that indistinguishable is symmetric in its last...	commit \| commitdiff \| tree
2015-02-20	Tim Makarios	Corrected a typo in the definition of indistinguishable	commit \| commitdiff \| tree
2015-02-19	Tim Makarios	Defined alternative indistinguishability_map	commit \| commitdiff \| tree
2015-02-19	Tim Makarios	Defined indistinguishable	commit \| commitdiff \| tree
2015-02-18	Tim Makarios	Proved that apply_encrypted_message_map doesn't mess...	commit \| commitdiff \| tree
2015-02-17	Tim Makarios	Defined self_encryption protocol	commit \| commitdiff \| tree
2015-02-17	Tim Makarios	Defined contains_message	commit \| commitdiff \| tree
2015-02-17	Tim Makarios	Proof that the meet of non_clairvoyant protocols is...	commit \| commitdiff \| tree
2015-02-17	Tim Makarios	Defined the Meet of a set of protocols	commit \| commitdiff \| tree
2015-02-13	Tim Makarios	Proof that timely_delivery requires no clairvoyance	commit \| commitdiff \| tree
2015-02-12	Tim Makarios	Simplified definition of timely_delivery protocol	commit \| commitdiff \| tree
2015-02-11	Tim Makarios	Defined relevant_subhistory to simplify non_clairvoyant	commit \| commitdiff \| tree
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