src/HOL/Auth/Shared.thy
changeset 16417 9bc16273c2d4
parent 15032 02aed07e01bf
child 17744 3007c82f17ca
equal deleted inserted replaced
16416:6061ae1f90f2 16417:9bc16273c2d4
     6 Theory of Shared Keys (common to all symmetric-key protocols)
     6 Theory of Shared Keys (common to all symmetric-key protocols)
     7 
     7 
     8 Shared, long-term keys; initial states of agents
     8 Shared, long-term keys; initial states of agents
     9 *)
     9 *)
    10 
    10 
    11 theory Shared = Event:
    11 theory Shared imports Event begin
    12 
    12 
    13 consts
    13 consts
    14   shrK    :: "agent => key"  (*symmetric keys*);
    14   shrK    :: "agent => key"  (*symmetric keys*);
    15 
    15 
    16 specification (shrK)
    16 specification (shrK)