Organization
============
 - `proofs`: proof scripts for some attacks
 - `5G_AKA.spthy`: Tamarin model of 5G-AKA with a binding channel between SN and HN
 - `5G_AKA.oracle`: Tamarin oracle for the proofs of 5G_AKA.spthy
 - `5G_AKA_fix.spthy`: Tamarin model of 5G-AKA with a binding channel between SN and HN, where SNID is included in MAC
 - `5G_AKA_fix.oracle`: Tamarin oracle for the proofs of 5G_AKA_fix.spthy
 - `analysis_results`: summary of trace properties of 5G-AKA with a binding channel between SN and HN
